3 Search Results for "Rümmer, Philipp"


Document
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
Integrated Deduction (Dagstuhl Seminar 21371)

Authors: Maria Paola Bonacina, Philipp Rümmer, and Renate A. Schmidt

Published in: Dagstuhl Reports, Volume 11, Issue 8 (2022)


Abstract
Logical reasoning plays a key role in fields as diverse as verification and synthesis, programming language foundations, knowledge engineering, and computer mathematics. Logical reasoning is increasingly important in intelligent systems, such as decision support systems, agent programming environments, and data processing systems, where deduction may provide explanation, course of action, and the capability of learning from missing information. Problem formalization in these domains typically involves multiple mathematical theories, knowledge bases, and ontologies, all of which may be very large. Problem solving requires both efficient automation and sophisticated human-machine interaction. The thrust of this seminar was that the key to unleash the power of computerized logical reasoning is integration, at different abstraction levels. This seminar offered a forum to discuss the issues related to integration of deduction in a diverse range of applications. In terms of reasoning procedures, the presence of both theories and quantifiers in problems from many contexts calls for methodologies to integrate state-of-the-art SMT solvers and automated theorem provers. This leads to investigate techniques such as model-based reasoning and semantic guidance, that were presented and discussed at the seminar. Similarly, the integration of inference rules for higher-order reasoning in inference systems that were born for first-order reasoning, such as superposition, was prominent among the topics debated at the seminar. At the architectural level, the sheer difficulty of the problems calls for the integration of provers and solvers into interactive reasoning environments. These range from higher-order proof assistants with background reasoners as hammers, to interactive program verifiers, both widely covered at the seminar in talks and discussions. The seminar showed how the application of deduction to intelligent systems necessitates the integration of deduction with other paradigms, such as probabilistic reasoning and statistical inferences. In fact, it emerged from the seminar that even systems that are not natively deductive, such as agent programming environments and industrial tools for ontology-based processing, benefit significantly from the integration of deduction. A clear and shared uptake from the seminar was that scalability and usability are crucial challenges at all levels of integration. The seminar fully succeded in promoting the exchange of new ideas and suggestions for future research.

Cite as

Maria Paola Bonacina, Philipp Rümmer, and Renate A. Schmidt. Integrated Deduction (Dagstuhl Seminar 21371). In Dagstuhl Reports, Volume 11, Issue 8, pp. 35-51, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@Article{bonacina_et_al:DagRep.11.8.35,
  author =	{Bonacina, Maria Paola and R\"{u}mmer, Philipp and Schmidt, Renate A.},
  title =	{{Integrated Deduction (Dagstuhl Seminar 21371)}},
  pages =	{35--51},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{8},
  editor =	{Bonacina, Maria Paola and R\"{u}mmer, Philipp and Schmidt, Renate A.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.11.8.35},
  URN =		{urn:nbn:de:0030-drops-157685},
  doi =		{10.4230/DagRep.11.8.35},
  annote =	{Keywords: Automated theorem proving, deduction, logic, reasoning, SMT solving}
}
Document
Deduction Beyond Satisfiability (Dagstuhl Seminar 19371)

Authors: Carsten Fuhs, Philipp Rümmer, Renate Schmidt, and Cesare Tinelli

Published in: Dagstuhl Reports, Volume 9, Issue 9 (2020)


Abstract
Research in automated deduction is traditionally focused on the problem of determining the satisfiability of formulas or, more generally, on solving logical problems with yes/no answers. Thanks to recent advances that have dramatically increased the power of automated deduction tools, there is now a growing interest in extending deduction techniques to attack logical problems with more complex answers. These include both problems with a long history, such as quantifier elimination, which are now being revisited in light of the new methods, as well as newer problems such as minimal unsatisfiable cores computation, model counting for propositional or first-order formulas, Boolean or SMT constraint optimization, generation of interpolants, abductive reasoning, and syntax-guided synthesis. Such problems arise in a variety of applications including the analysis of probabilistic systems (where properties like safety or liveness can be established only probabilistically), network verification (with relies on model counting), the computation of tight complexity bounds for programs, program synthesis, model checking (where interpolation or abductive reasoning can be used to achieve scale), and ontology-based information processing. The seminar brought together researchers and practitioners from many of the often disjoint sub-communities interested in the problems above. The unifying theme of the seminar was how to harness and extend the power of automated deduction methods to solve problems with more complex answers than binary ones.

Cite as

Carsten Fuhs, Philipp Rümmer, Renate Schmidt, and Cesare Tinelli. Deduction Beyond Satisfiability (Dagstuhl Seminar 19371). In Dagstuhl Reports, Volume 9, Issue 9, pp. 23-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@Article{fuhs_et_al:DagRep.9.9.23,
  author =	{Fuhs, Carsten and R\"{u}mmer, Philipp and Schmidt, Renate and Tinelli, Cesare},
  title =	{{Deduction Beyond Satisfiability (Dagstuhl Seminar 19371)}},
  pages =	{23--44},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2020},
  volume =	{9},
  number =	{9},
  editor =	{Fuhs, Carsten and R\"{u}mmer, Philipp and Schmidt, Renate and Tinelli, Cesare},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.9.9.23},
  URN =		{urn:nbn:de:0030-drops-118432},
  doi =		{10.4230/DagRep.9.9.23},
  annote =	{Keywords: abduction, automated deduction, interpolation, quantifier elimination, synthesis}
}
  • Refine by Author
  • 2 Rümmer, Philipp
  • 1 Blanchette, Jasmin
  • 1 Bonacina, Maria Paola
  • 1 Desharnais, Martin
  • 1 Fuhs, Carsten
  • Show More...

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

  • Refine by Keyword
  • 1 Automated theorem proving
  • 1 Automatic theorem proving
  • 1 SMT solving
  • 1 abduction
  • 1 automated deduction
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 2 2022
  • 1 2020

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