Logic List Mailing Archive
CfP: IJCAR 2024: The 12th International Joint Conference on Automated Reasoning, 1-6 July 2024. Nancy (France)
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 <quantify24@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.france@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.france@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)
--
[LOGIC] mailing list, provided by DLMPST
More information (including information about subscription management) can
be found here: http://dlmpst.org/pages/logic-list.php