Search Results

Documents authored by Desharnais, Martin

Document
DOI: 10.4230/LIPIcs.ITP.2024.12
A Modular Formalization of Superposition in Isabelle/HOL

Authors: Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette, and Sophie Tourret

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
Superposition is an efficient proof calculus for reasoning about first-order logic with equality that is implemented in many automatic theorem provers. It works by saturating the given set of clauses and is refutationally complete, meaning that if the set is inconsistent, the saturation will contain a contradiction. In this work, we restructured the completeness proof to cleanly separate the ground (i.e., variable-free) and nonground aspects, and we formalized the result in Isabelle/HOL. We relied on the IsaFoR library for first-order terms and on the Isabelle saturation framework.
Cite as

Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette, and Sophie Tourret. A Modular Formalization of Superposition in Isabelle/HOL. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.ITP.2024.12,
  author =	{Desharnais, Martin and Toth, Balazs and Waldmann, Uwe and Blanchette, Jasmin and Tourret, Sophie},
  title =	{{A Modular Formalization of Superposition in Isabelle/HOL}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{12:1--12:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.12},
  URN =		{urn:nbn:de:0030-drops-207401},
  doi =		{10.4230/LIPIcs.ITP.2024.12},
  annote =	{Keywords: Superposition, verification, first-order logic, higher-order logic}
}
Document
DOI: 10.4230/DagRep.13.11.130
The Next Generation of Deduction Systems: From Composition to Compositionality (Dagstuhl Seminar 23471)

Authors: Maria Paola Bonacina, Pascal Fontaine, Cláudia Nalon, Claudia Schon, and Martin Desharnais

Published in: Dagstuhl Reports, Volume 13, Issue 11 (2024)

Abstract
Deduction systems are computer procedures that employ inference or transition rules, search strategies, and multiple supporting algorithms, to solve problems by logico-deductive reasoning. They are at the heart of SAT/SMT solvers, theorem provers, and proof assistants. The wide range of successful applications of these tools shows how logico-deductive reasoning is well-suited for machines. Nonetheless, satisfiability and validity are difficult problems, and applications require reasoners to handle large and heterogeneous knowledge bases, and to generate proofs and models of increasing size and diversity. Thus, a vast array of techniques was developed, leading to what was identified during the seminar as a crisis of growth. This crisis manifests itself also as a software crisis, called automated reasoning software crisis at the seminar. Many deduction systems remain prototypes, while relatively few established systems resort to assemble techniques into portfolios that are useful for experiments, but do not lead to breakthroughs. In order to address this crisis of growth, the Dagstuh Seminar "The Next Generation of Deduction Systems: From Composition to Compositionality" (23471) focused on the key concept of composition, that is, a combination where properties of the components are preserved. Composition applies to all building blocks of deduction: rule systems, strategies, proofs, and models. All these instances of compositions were discussed during the seminar, including for example composition of instance-based and superposition-based inference systems, and composition of modules towards proof production in SMT solvers. Other kinds of composition analyzed during the seminar include the composition of reasoning and learning, and the composition of reasoning systems and knowledge systems. Indeed, reasoners learn within and across derivations, while for applications, from verification to robotics, provers and solvers need to work with other knowledge-based components. In order to address the automated reasoning software crisis, the seminar elaborated the concept of compositionality, as the engineering counterpart of what is composition at the theory and design levels. The seminar clearly identified modularity as the first step towards compositionality, proposing to decompose existing systems into libraries of modules that can be recomposed in new systems. The ensuing discussion led to the distinction between automated reasoners that are industry powertools and automated reasoners that are pedagogical tools. At the societal level, this distinction is important to counter the phenomenon whereby new students are either discouraged by the impossibility of competing with industry powertools, or induced to join only those research groups that work on industry powertools. In summary, the seminar fully succeeded in promoting the exchange of ideas and suggestions for future work.
Cite as

Maria Paola Bonacina, Pascal Fontaine, Cláudia Nalon, Claudia Schon, and Martin Desharnais. The Next Generation of Deduction Systems: From Composition to Compositionality (Dagstuhl Seminar 23471). In Dagstuhl Reports, Volume 13, Issue 11, pp. 130-150, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{bonacina_et_al:DagRep.13.11.130,
  author =	{Bonacina, Maria Paola and Fontaine, Pascal and Nalon, Cl\'{a}udia and Schon, Claudia and Desharnais, Martin},
  title =	{{The Next Generation of Deduction Systems: From Composition to Compositionality (Dagstuhl Seminar 23471)}},
  pages =	{130--150},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{11},
  editor =	{Bonacina, Maria Paola and Fontaine, Pascal and Nalon, Cl\'{a}udia and Schon, Claudia and Desharnais, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.11.130},
  URN =		{urn:nbn:de:0030-drops-198472},
  doi =		{10.4230/DagRep.13.11.130},
  annote =	{Keywords: artificial intelligence, automated reasoning, compositionality, deduction, logic}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.8
Seventeen Provers Under the Hammer

Authors: Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
One of the main success stories of automatic theorem provers has been their integration into proof assistants. Such integrations, or "hammers," increase proof automation and hence user productivity. In this paper, we use Isabelle/HOL’s Sledgehammer tool to find out how useful modern provers are at proving formulas in higher-order logic. Our evaluation follows in the steps of Böhme and Nipkow’s Judgment Day study from 2010, but instead of three provers we use 17, including SMT solvers and higher-order provers. Our work offers an alternative yardstick for comparing modern provers, next to the benchmarks and competitions emerging from the TPTP World and SMT-LIB.
Cite as

Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel. Seventeen Provers Under the Hammer. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.ITP.2022.8,
  author =	{Desharnais, Martin and Vukmirovi\'{c}, Petar and Blanchette, Jasmin and Wenzel, Makarius},
  title =	{{Seventeen Provers Under the Hammer}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.8},
  URN =		{urn:nbn:de:0030-drops-167178},
  doi =		{10.4230/LIPIcs.ITP.2022.8},
  annote =	{Keywords: Automatic theorem proving, interactive theorem proving, proof assistants}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact