IJCAR 2024 --- Co-Located workshops. More information below. PAAR-2024: 9TH WORKSHOP ON PRACTICAL ASPECTS OF AUTOMATED REASONING https://paar2024.github.io/
QUANTIFY 2024: International Workshop on Quantification https://qbf24.pages.sai.jku.at/quantify/ SC-Square 2024: 9th International Workshop on Satisfiability Checking and Symbolic Computation http://www.sc-square.org/CSA/workshop9.html Termination and Complexity Competition 2024 http://www.termination-portal.org/wiki/Termination_Competition_2024 ThEdu'24: Theorem proving components for Educational software http://www.uc.pt/en/congressos/thedu/ThEdu24 UNIF 2024: The 38th International Workshop on Unification https://lat.inf.tu-dresden.de/unif2024 5th International Workshop on Automated (Co)inductive Theorem Proving https://wait2024.github.io/ The TPTP Tea Party https://www.tptp.org/TPTP/TPTPTParty/2024/ ****************************************************************************** PAAR-2024: 9TH WORKSHOP ON PRACTICAL ASPECTS OF AUTOMATED REASONING -- co-located with IJCAR 2024 -- July 2, 2024, Nancy, France Web site: https://paar2024.github.io/ Submission link: https://easychair.org/conferences/?conf=paar2024 Abstract registration deadline: April 5, 2024 Submission deadline: April 12, 2024 Topics: automated reasoning, implementation, tools ****************************************************************************** The automation of logical reasoning is a challenge that has been studied intensively in fields including mathematics, philosophy, and computer science. PAAR is the workshop on turning this theory into practice: how can automated reasoning tools be built that work and are useful in applications? PAAR covers all aspects of this challenge: which theories, logics, or fragments are well-behaved in practice, and connect well to application domains? which reasoning tasks are tractable and useful? which algorithms are able to solve real-world instances? how should automated reasoning tools be designed, implemented, tested, and evaluated? The goal of PAAR is to bring together theoreticians, tool developers, and users, to concentrate on the practical aspects of automated reasoning. The workshop welcomes high-quality contributions of any kind, including new research results, presentation of work in progress, presentation of new tools, new implementation techniques, new application domains, or case studies. Submission Guidelines --------------------- Researchers interested in participating are invited to submit either an extended abstract (up to 8 pages) or a regular paper (up to 15 pages), excluding references, via EasyChair at https://easychair.org/conferences/?conf=paar2024. Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Short submissions that could stimulate fruitful discussion at the workshop are particularly welcome. Submissions should be prepared in LaTeX using the CEUR-WS.org style template (CEURART, one-column). The package containing the class file and the user guide can be downloaded from http://ceur-ws.org/Vol-XXX/CEURART.zip. Topics include, but are not limited to: -------------------------------------- * automated reasoning in propositional, first-order, higher-order, and non-classical logics; * implementation of provers (SAT, SMT, resolution, superposition, tableau, instantiation-based, rewriting, logical frameworks, etc.); * automated reasoning tools for all kinds of practical problems and applications; * pragmatics of automated reasoning within proof assistants; * practical experiences, usability aspects, feasibility studies; * evaluation of implementation techniques and automated reasoning tools; * performance aspects, benchmarking approaches; non-standard approaches to automated reasoning, non-standard forms of automated reasoning, new applications; * implementation techniques, optimisation techniques, machine learning, strategies and heuristics, fairness; * tools or methods that support prover development; * system descriptions and demos. Invited Speakers ------------------- * N.N. * N.N. Programme Committee ------------------- * Cláudia Nalon, University of BrasÃlia, BR (PC co-chair) * Alexander Steen, University of Greifswald, DE (PC co-chair) * Martin Suda, Czech Technical University in Prague, CZ (PC co-chair) * to be completed Publication ----------- PAAR proceedings will be published electronically in a workshop proceedings venue (such as CEUR workshop proceedings or EasyChair Kalpa proceedings). Venue ----- IJCAR 2024 in Nancy, France Important dates --------------- * Abstract submission: April 5, 2024 * Paper submission: April 12, 2024 * Workshop: July 2, 2024 ****************************************************************************** International Workshop on Quantification (QUANTIFY 2024) (co-located with the International Joint Conference on Automated Reasoning) https://qbf24.pages.sai.jku.at/quantify/ ****************************************************************************** *** Overview *** Quantifiers play an important role in language extensions of many logics. The use of quantifiers often allows for a more succinct encoding as it would be possible without quantifiers. However, the introduction of quantifiers affects the complexity of the extended formalism in general. In consequence, theoretical results established for the quantifier-free formalism may not directly be transferred to the quantified case. Further, techniques successfully implemented in reasoning tools for quantifier-free formulas cannot directly be lifted to a quantified version. The goal of the Workshop on Quantification (QUANTIFY 2024) is to bring together researchers who investigate the impact of quantification from a theoretical as well as from a practical point of view. Quantification is a topic in different research areas, e.g., in SAT in terms of QBF, in CSP in terms of QCSP, in SMT, ATP, Computer Algebra, etc. This workshop has the aim to provide an interdisciplinary forum where researchers of various fields may exchange their experiences. In particular, the following topics shall be considered at the workshop: * Theoretical aspects of quantification. * Practical aspects of quantification. * Intersections between the different research communities working on quantification. *** Organizers *** * Konstantin Korovin, University of Manchester, UK * Martina Seidl, Johannes Kepler University Linz, Austria *** Program Committee *** * Konstantin Korovin, University of Manchester, UK * Martina Seidl, Johannes Kepler University Linz, Austria TBA *** Important Dates *** Paper Submission: May 1 Notification of Acceptance: May 21 Camera Ready: June 1 Workshop: July 1 *** Submission *** Submissions of extended abstracts, full papers, and tutorials are solicited and will be managed via Easychair: https://easychair.org/conferences/?conf=quantify24 Submitted papers should be formatted in LNCS format. We solicit three types of submissions: * Talk abstracts (maximum two pages, excluding references) describing already published results. * Full papers (maximum 15 pages, excluding references) on novel, unpublished work. * Tutorial papers (maximum 15 pages, excluding references) introducing a research field related to quantifiers. The talk abstracts should include a relevant bibliography of related work and an outline of the planned talk. For this category, we explicitly advocate talks which summarize the results of one or more already published papers. Full papers should contain novel, unpublished work that qualifies to be published in a special issue of a journal or formal workshop proceedings. Tutorial papers should survey results already published, maybe in multiple articles or presentations capturing the commonalities and differences of various quantification approaches (perhaps even interdisciplinary). Each submission will be assessed by the program committee and the workshop organizers with respect to novelty, originality, and scope. Submissions related to completed work as well as work in progress are welcome. Authors are encouraged to provide additional material such as source code of tools, experimental data, benchmarks and related publications in an appendix or a related webpage. The additional material will be considered at the discretion of the reviewers. Previously published work or extensions thereof may be submitted to the workshop but that case has to be explicitly stated in the submitted paper. This regulation also applies to work which is currently under review elsewhere. Authors of accepted abstracts and papers are expected to give a talk at the workshop. *** Plans for Publications *** The outcomes of the discussions will be summarized in a workshop report, which can be made publicly available as technical report (unless the participants decide not to do so). In case we get enough full and tutorial papers, we will organize a special issue on quantification (e.g., in the Journal of Satisfiability (JSAT) or formal workshop proceedings. *** Contact *** For any questions, contact <quantif...@easychair.org>. ****************************************************************************** 9th International Workshop on Satisfiability Checking and Symbolic Computation SC-Square 2024 July 2, 2024, Nancy France http://www.sc-square.org/CSA/workshop9.html ****************************************************************************** The 9th SC-Square Workshop is a satellite event of IJCAR, held at the Inria Nancy research center and LORIA in Nancy, France, from July 1 to July 6, 2024. Main conference website: https://merz.gitlabpages.inria.fr/2024-ijcar/ SC-Square Workshop website: http://www.sc-square.org/CSA/workshop9.html === Keynote Speakers === We are pleased to announce our keynote speakers: - Manuel Kauers (Johannes Kepler University, Austria) - Lawrence Paulson (University of Cambridge, UK) === Key Dates === Submission deadline: April 12, 2024 ISSAC Fast-Track Deadline*: May 3, 2024 Notification: May 17, 2024 Final version: May 31, 2024 Workshop date: July 2, 2024 *This year, considering the rather tight schedule between the ISSAC conference authors notification (April 30) and the workshop (July 2), we will allow an ISSAC fast track for papers, i.e., (1) papers that do not make it to ISSAC on topics related to SC-Square will have the opportunity to be submitted late to SC-Square as full papers; (2) papers that do make it to ISSAC on topics related to SC-Square will have the opportunity to be submitted late to SC-Square as presentation-only papers. === Scope === Symbolic Computation is concerned with the efficient algorithmic determination of exact solutions to complicated mathematical problems. Satisfiability Checking has recently started to tackle similar problems but with different algorithmic and technological solutions. The two communities share many central interests, but researchers from these two communities rarely interact. Also, the lack of common or compatible interfaces for tools is an obstacle to their fruitful combination. Bridges between the communities in the form of common platforms and road-maps are necessary to initiate an exchange, and to support and direct their interaction. The aim of this workshop is to provide an opportunity to discuss, share knowledge and experience across both communities. === Submitting to the Workshop === The workshop series has emerged from an H2020 FETOPEN CSA project "SC-Square", which ran from 2016 to 2018. It has been continued aiming at building bridges bewteen Satisfiability Checking and Symbolic Computation. It is open for submission and participation to everyone interested in the topics, whether or not they were members or associates of the original project. The topics of interest include but are not limited to: - Satisfiability Checking for Symbolic Computation - Symbolic Computation for Satisfiability Checking - Applications relying on both Symbolic Computation and Satisfiability Checking - Combination of Symbolic Computation and Satisfiability Checking tools - Quantifier elimination and decision procedures and their embedding into logic provers, including but not limited to SMT solvers, and computer algebra software ==== Submission guidelines ==== Submissions should be in English, formatted in Springer LNCS style and submitted via EasyChair using this link: https://easychair.org/conferences/?conf=scsquare2024 We invite three types of submissions: (1) FULL PAPERS on research, case studies or tool development should present unpublished work not submitted elsewhere (with a limit of 16 pages, not counting references) (2) EXTENDED ABSTRACTS on research, case studies or tool development should present unpublished (potentially ongoing) work not submitted elsewhere (2â4 pages, not counting references) (3) PRESENTATION-ONLY submissions on already published work, work to be published elsewhere, or work in progress on SC-Square related open problems or future challenges. Please submit an abstract for approval by the PC (with a limit of 2 pages). To receive the appropriate level of peer review, please declare your category of your submission by prefixing the title on the EasyChair form with "FP", "EA" or "PO" accordingly. For consistency, all submissions must use the LNCS style. Current llncs latex files are available from " LaTeX2e Proceedings Templates download" at: https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines We plan to publish the proceedings of the workshop digital form, hosted with CEUR-WS (see http://ceur-ws.org/). Authors may opt out of this, should they prefer to publish the material elsewhere. People from industry and business are warmly invited to submit papers to describe their problems, challenges, goals, and expectations for the SC-square community. === Workshop Co-Chairs === Daniela Kaufmann (TU Wien, AT) Chris Brown (U. S. Naval Academy, USA) === Program Committee === Erika Abraham (RWTH Aachen University, DE) Haniel Barbosa (Universidade Federal de Minas Gerais, BR) Armin Biere (University of Freiburg, DE) Anna Bigatti (University of Genova, IT) Martin Brain (City University of London, UK) Curtis Bright (University of Waterloo, CA) David Cerna (Institute of Computer Science, Czech Academy of Sciences, CZ) James H. Davenport (University of Bath, UK) Matthew England (Coventry University, UK) Pascal Fontaine (University of Liege, BE) Alberto Griggio (Fondazione Bruno Kessler, IT) Mikolas Janota (Czech Technical University in Prague, CZ) Konstantin Korovin (The University of Manchester, UK) Ilias Kotsireas (Wilfrid Laurier University, CA & Maplesoft) Gereon Kremer (Certora, IL) Alex Ozdemir (Stanford University, US) Stefan Ratschan (Institute of Computer Science, Czech Academy of Sciences, CZ) Christoph Scholl (University of Freiburg, DE) Thomas Sturm (CNRS, FR & MPI Informatics, DE) Bican Xia (Peking University, CN) ****************************************************************************** Termination and Complexity Competition 2024 http://www.termination-portal.org/wiki/Termination_Competition_2024 Call for Participation ****************************************************************************** Since the beginning of the millennium, many research groups developed tools for fully automated termination and complexity analysis. After a tool demonstration at the 2003 Termination Workshop in Valencia, the community decided to start an annual termination competition to spur the development of tools and termination techniques. The termination and complexity competition focuses on automated termination and complexity analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programming, logic programming, and functional programming. In all categories, we also welcome the participation of tools providing certifiable proofs. The goal of the termination and complexity competition is to demonstrate the power of the leading tools in each of these areas. The competition will be affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2024, https://merz.gitlabpages.inria.fr/2024-ijcar/). It will be run on the StarExec platform (https://www.starexec.org/). The final run and a presentation of the final results will be live at IJCAR. We strongly encourage all developers of termination and complexity analysis tools to participate in the competition. We also welcome the submission of termination and complexity problems, especially problems that come from applications. A category is only run in the competition if there are at least 2 participants and at least 40 examples for this category in the underlying termination problem data base. If there is no category that is convenient for your tool, you can contact the organizers, since other categories can be considered as well if enough participants are guaranteed. For further information, we refer to the website of the termination and complexity competition: https://termination-portal.org/wiki/Termination_Competition_2024 Important dates Tool and Benchmark Submission: June 12, 2024 First Run: June 19, 2024 Bugfix Deadline: June 26, 2024 IJCAR: July 3-6, 2024 ************************************************************************* ThEdu'24 Theorem proving components for Educational software 2 July 2024 http://www.uc.pt/en/congressos/thedu/ThEdu24 ************************************************************************* THedu'24 Scope: Computer Theorem Proving is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of a new software generation and to discuss existing systems. Important Dates * Extended Abstracts: 10 April 2024 * Author Notification: 8 May 2024 * Workshop Day: 2 July 2024 Topics of interest include: * interactive and automated theorem provers designed or adapted for education; * methods of automated deduction applied to checking students' input; * combinations of deduction and computation enabling systems to propose next step guidance; * combination of symbolic artificial intelligence and machine learning for the teaching of proof and proving; * design of libraries of statements and/or formal proofs for use in educational systems; * graphical user interfaces for theorem proving in the classroom; * specific systems integrated in educational components such as dynamic geometry software, automatic provers providing readable output or explicit counter examples, etc.; * the role of logic and formal systems in the didactic of proof and proving in mathematics education; * experience reports about the use of automatic or interactive theorem provers for teaching. Submission We welcome submission of extended abstracts and demonstration proposals presenting original unpublished work which is not been submitted for publication elsewhere. All accepted extended abstracts and demonstrations will be presented at the workshop. Abstracts will be made available online. Extended abstracts and demonstration proposals should be submitted via easychair, https://easychair.org/conferences/?conf=thedu24 formatted according to http://www.easychair.org/publications/easychair.zip Extended abstracts and demonstration proposals should be 5-10 pages in length and are to be submitted in PDF format. At least one of the authors of each accepted extended abstract/demonstration proposal is expected to attend THedu'24 and presents their extended abstract/demonstration. Program Committee (tentative) David Cerna, Johannes Kepler University, Austria Joao Marcos, Federal University of Rio Grande do Norte, Brazil Filip Maric, University of Belgrade, Serbia Julien Narboux, University of Strasbourg, France, (co-chair) Walther Neuper, Johannes Kepler University, Linz, Austria (co-chair) Pedro Quaresma, University of Coimbra, Portugal (co-chair) Philppe R. Richard, University of Montréal, Canada Vanda Santos, University of Aveiro, Portugal Anders Schlichtkrull, Aalborg University, Denmark Wolfgang Schreiner, Johannes Kepler University, Austria Athina Thoma, University of Southampton, UK M. Pilar Velez, Nebrija University, Spain Jorgen Villadsen, Technical University of Denmark, Denmark Kitty Yan, University of Toronto, Canada Proceedings Abstracts and system descriptions will be available in ThEdu'24 Web-wage. After the Workshop an open call for papers will be issued. It is expected that authors of accepted extended abstract can submit a substantially revised version, extended to 14-20 pages, for publication by the Electronic Proceedings in Theoretical Computer Science (EPTCS). UNIF 2024 Call for Papers ****************************************************************************** Call for Papers UNIF 2024 The 38th International Workshop on Unification Nancy, France, July 2, 2024 A satellite workshop of CADE/IJCAR, affiliated with IJCAR https://lat.inf.tu-dresden.de/unif2024 ****************************************************************************** UNIF 2024 is the 38th event in a series of international meetings devoted to unification theory and its applications. Unification is concerned with the problem of making two given terms equal, either syntactically or modulo an equational theory. It is a fundamental process used in various areas of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, knowledge representation, types, etc. The International Workshop on Unification (UNIF) is a forum for researchers in unification theory and related fields to present recent (even unfinished) work, and to discuss new ideas and trends. It is also a good opportunity for students, young researchers and scientists working in related areas to get an overview of the current state of the art in unification theory. Topics ------ A non-exhaustive list of topics of interest includes: * syntactic and equational unification algorithms * matching and constraint solving * higher-order unification * unification in modal, temporal, and description logics * admissibility of inference rules * narrowing * disunification * anti-unification * complexity issues * combination methods * implementation techniques * applications Submission ---------- Short papers or extended abstracts, up to 5 pages in EasyChair style, should be submitted electronically as PDF files through the EasyChair submission site: https://easychair.org/conferences/?conf=unif2024 Abstracts will be evaluated by the Program Committee regarding their significance for the workshop. We allow submissions of work presented/ submitted in/to another conference. Accepted abstracts will be presented at the workshop and included in the informal proceedings of the workshop, available in electronic form on the Web page of UNIF 2024. At least one of the authors should register for the workshop. Based on the number and quality of submissions we will decide whether to organize a special journal issue. Important Dates --------------- * Paper submission: April 18, 2024 (AoE) * Author notification: May 23, 2024 (AoE) * Camera-ready version: June 7, 2024 (AoE) * UNIF 2024: July 2, 2024 Invited Speakers ---------------- To be announced. ****************************************************************************** 5th International Workshop on Automated (Co)inductive Theorem Proving ****************************************************************************** We are delighted to announce the Fifth International Workshop on Automated (Co)inductive Theorem Proving, an event dedicated to the latest developments in inductive and coinductive methods for verification. This workshop is a significant gathering for researchers and practitioners in the field, providing an invaluable opportunity to explore current challenges and innovations in computational verification. Key Themes: Advances in inductive reasoning for recursive structures and loop-containing programs. Developments in coinductive methods and their growing relevance in verification and industrial applications. Cross-disciplinary collaboration to foster innovation in computational verification methods, including SMT, HOL, FOL, etc. Featured Speakers Announcement: We are thrilled to announce that this year's workshop will feature at least two distinguished invited speakers: Prof. Dmitriy Traytel from the University of Copenhagen and Dr. Stefan Hetzl from the Vienna University of Technology. Call for Abstracts: We invite you to submit an extended abstract showcasing your latest research, findings, or ongoing studies in the field of automated (co)inductive theorem proving. This is a fantastic platform to share your work with a diverse and expert audience, engage in intellectual exchange, and contribute to the advancement of the field. We welcome studies and findings published within the last five years. Submission Guidelines: abstracts are to be sent to wait.in.fra...@gmail.com Length: 1-2 pages excluding references. Recommended Format: easychair.cls Important Dates: Abstract Submission Deadline: 15 May. Notification of Acceptance: 1 June. Workshop Format: The workshop will feature in-depth tutorials, talks by leading experts, and a panel discussion for interactive dialogue. It is an ideal setting for networking, collaboration, and gaining new insights into the challenges and opportunities in automated theorem proving. Remote Participation: While on-site attendance is encouraged to fully benefit from the interactive nature of the workshop, provisions for remote participation will be available for wider accessibility. Dissemination and Special Issue: Selected abstracts and presentation slides will be published on the workshop website. There's also a plan for a special journal issue based on the workshop's theme, subject to participant interest. Join Us: Be a part of this stimulating event to discuss, learn, and contribute to the future of automated (co)inductive theorem proving. Donât miss this opportunity to engage with a vibrant community and shape the future of verification techniques. We look forward to your submissions and participation! For more information, please visit the workshop website (https://wait2024.github.io/) or contact the organizers, Yutaka Nagashima and Sorin Stratulat at wait.in.fra...@gmail.com. ****************************************************************************** TPTP Tea Party ****************************************************************************** The TPTP Tea Party brings together developers and users of the TPTP World, including (but not limited to): * The TPTP problem library and the TSTP solution library * The TPTP languages, problem formats, and solution formats * The SZS ontology * SystemOnTPTP * The CADE ATP System Competition (CASC) * etc The meeting aims to elicit feedback, suggestions, criticisms, etc, of these resources, in order to ensure that their continued development meets the needs of successful automated reasoning. The meeting will be structured discussion following an agenda of topics that have been suggested and agreed upon in advance. This year funding for participants is provided by Working Group 2 Automated Theorem Provers, COST Action 2011 EuroProofNet. If you would like to receive announcements about the meeting, funding, and more, please join the TPTP World Google Group (https://groups.google.com/g/tptp-world)
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
