4 Search Results for "Fontaine, Pascal"

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-dev.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}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.5
Efficient Full Higher-Order Unification

Authors: Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
We developed a procedure to enumerate complete sets of higher-order unifiers based on work by Jensen and Pietrzykowski. Our procedure removes many redundant unifiers by carefully restricting the search space and tightly integrating decision procedures for fragments that admit a finite complete set of unifiers. We identify a new such fragment and describe a procedure for computing its unifiers. Our unification procedure is implemented in the Zipperposition theorem prover. Experimental evaluation shows a clear advantage over Jensen and Pietrzykowski’s procedure.
Cite as

Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin. Efficient Full Higher-Order Unification. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{vukmirovic_et_al:LIPIcs.FSCD.2020.5,
  author =	{Vukmirovi\'{c}, Petar and Bentkamp, Alexander and Nummelin, Visa},
  title =	{{Efficient Full Higher-Order Unification}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{5:1--5:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.5},
  URN =		{urn:nbn:de:0030-drops-123271},
  doi =		{10.4230/LIPIcs.FSCD.2020.5},
  annote =	{Keywords: unification, higher-order logic, theorem proving, term rewriting, indexing data structures}
}
Document
DOI: 10.4230/DagRep.5.11.71
Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471)

Authors: Erika Ábrahám, Pascal Fontaine, Thomas Sturm, and Dongming Wang

Published in: Dagstuhl Reports, Volume 5, Issue 11 (2016)

Abstract
The seminar focused on satisfiability checking for combinations of first-order logic and subclasses thereof with arithmetic theories in a very liberal sense, also covering quantifiers and parameters. It gathered members of the two communities of symbolic computation (or computer algebra) and satisfiability checking (including satisfiability modulo theories). Up-to-now, these two communities have been working quite independently. We are confident that the seminar will initiate cross-fertilization of both fields and bring improvements for both satisfiability checking and symbolic computation, and for their applications.
Cite as

Erika Ábrahám, Pascal Fontaine, Thomas Sturm, and Dongming Wang. Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471). In Dagstuhl Reports, Volume 5, Issue 11, pp. 71-89, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{abraham_et_al:DagRep.5.11.71,
  author =	{\'{A}brah\'{a}m, Erika and Fontaine, Pascal and Sturm, Thomas and Wang, Dongming},
  title =	{{Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471)}},
  pages =	{71--89},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{11},
  editor =	{\'{A}brah\'{a}m, Erika and Fontaine, Pascal and Sturm, Thomas and Wang, Dongming},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.11.71},
  URN =		{urn:nbn:de:0030-drops-57657},
  doi =		{10.4230/DagRep.5.11.71},
  annote =	{Keywords: algorithmic algebra, arithmetic, automated reasoning, decision procedures, quantifier elimination, satisfiability checking, SMT solving, symbolic comp}
}
  • Refine by Author
  • 2 Desharnais, Martin
  • 2 Fontaine, Pascal
  • 2 Vukmirović, Petar
  • 1 Bentkamp, Alexander
  • 1 Blanchette, Jasmin
  • Show More...

  • Refine by Classification
  • 2 Computing methodologies → Theorem proving algorithms
  • 1 Theory of computation → Automated reasoning

  • Refine by Keyword
  • 2 automated reasoning
  • 1 Automatic theorem proving
  • 1 SMT solving
  • 1 algorithmic algebra
  • 1 arithmetic
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 1 2016
  • 1 2020
  • 1 2022
  • 1 2024

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