4 Search Results for "Schmidt, Renate A."

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/DagMan.10.1.1
Current and Future Challenges in Knowledge Representation and Reasoning (Dagstuhl Perspectives Workshop 22282)

Authors: James P. Delgrande, Birte Glimm, Thomas Meyer, Miroslaw Truszczynski, and Frank Wolter

Published in: Dagstuhl Manifestos, Volume 10, Issue 1 (2024)

Abstract
Knowledge Representation and Reasoning is a central, longstanding, and active area of Artificial Intelligence. Over the years it has evolved significantly; more recently it has been challenged and complemented by research in areas such as machine learning and reasoning under uncertainty. In July 2022,sser a Dagstuhl Perspectives workshop was held on Knowledge Representation and Reasoning. The goal of the workshop was to describe the state of the art in the field, including its relation with other areas, its shortcomings and strengths, together with recommendations for future progress. We developed this manifesto based on the presentations, panels, working groups, and discussions that took place at the Dagstuhl Workshop. It is a declaration of our views on Knowledge Representation: its origins, goals, milestones, and current foci; its relation to other disciplines, especially to Artificial Intelligence; and on its challenges, along with key priorities for the next decade.
Cite as

James P. Delgrande, Birte Glimm, Thomas Meyer, Miroslaw Truszczynski, and Frank Wolter. Current and Future Challenges in Knowledge Representation and Reasoning (Dagstuhl Perspectives Workshop 22282). In Dagstuhl Manifestos, Volume 10, Issue 1, pp. 1-61, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{delgrande_et_al:DagMan.10.1.1,
  author =	{Delgrande, James P. and Glimm, Birte and Meyer, Thomas and Truszczynski, Miroslaw and Wolter, Frank},
  title =	{{Current and Future Challenges in Knowledge Representation and Reasoning (Dagstuhl Perspectives Workshop 22282)}},
  pages =	{1--61},
  journal =	{Dagstuhl Manifestos},
  ISSN =	{2193-2433},
  year =	{2024},
  volume =	{10},
  number =	{1},
  editor =	{Delgrande, James P. and Glimm, Birte and Meyer, Thomas and Truszczynski, Miroslaw and Wolter, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagMan.10.1.1},
  URN =		{urn:nbn:de:0030-drops-201403},
  doi =		{10.4230/DagMan.10.1.1},
  annote =	{Keywords: Knowledge representation and reasoning, Applications of logics, Declarative representations, Formal logic}
}
Document
DOI: 10.4230/DagRep.11.8.35
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.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
DOI: 10.4230/DagRep.9.9.23
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.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 Delgrande, James P.
  • 1 Desharnais, Martin
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 1 Applications of logics
  • 1 Automated theorem proving
  • 1 Declarative representations
  • 1 Formal logic
  • 1 Knowledge representation and reasoning
  • Show More...

  • Refine by Type
  • 4 document

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

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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact