Search Results

Documents authored by Fuhs, Carsten

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}
}
Document
DOI: 10.4230/DagRep.7.9.26
Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)

Authors: Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, and Cesare Tinelli

Published in: Dagstuhl Reports, Volume 7, Issue 9 (2018)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 17371 "Deduction Beyond First-Order Logic." Much research in the past two decades was dedicated to automating first-order logic with equality. However, applications often need reasoning beyond this logic. This includes genuinely higher-order reasoning, reasoning in theories that are not finitely axiomatisable in first-order logic (such as those including transitive closure operators or standard arithmetic on integers or reals), or reasoning by mathematical induction. Other practical problems need a mixture of first-order proof search and some more advanced reasoning (for instance, about higher-order formulas), or simply higher-level reasoning steps. The aim of the seminar was to bring together first-order automated reasoning experts and researchers working on deduction methods and tools that go beyond first-order logic. The seminar was dedicated to the exchange of ideas to facilitate the transition from first-order to more expressive settings.
Cite as

Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, and Cesare Tinelli. Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371). In Dagstuhl Reports, Volume 7, Issue 9, pp. 26-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{blanchette_et_al:DagRep.7.9.26,
  author =	{Blanchette, Jasmin Christian and Fuhs, Carsten and Sofronie-Stokkermans, Viorica and Tinelli, Cesare},
  title =	{{Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)}},
  pages =	{26--46},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{7},
  number =	{9},
  editor =	{Blanchette, Jasmin Christian and Fuhs, Carsten and Sofronie-Stokkermans, Viorica 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.7.9.26},
  URN =		{urn:nbn:de:0030-drops-85872},
  doi =		{10.4230/DagRep.7.9.26},
  annote =	{Keywords: Automated Deduction, Program Verification, Certification}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.176
Polynomial Interpretations for Higher-Order Rewriting

Authors: Carsten Fuhs and Cynthia Kop

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent years. We adapt and extend this method to the alternative formalism of algebraic functional systems, where the simply-typed lambda-calculus is combined with algebraic reduction. Using this theory, we define higher-order polynomial interpretations, and show how the implementation challenges of this technique can be tackled. A full implementation is provided in the termination tool Wanda.
Cite as

Carsten Fuhs and Cynthia Kop. Polynomial Interpretations for Higher-Order Rewriting. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 176-192, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{fuhs_et_al:LIPIcs.RTA.2012.176,
  author =	{Fuhs, Carsten and Kop, Cynthia},
  title =	{{Polynomial Interpretations for Higher-Order Rewriting}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{176--192},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.176},
  URN =		{urn:nbn:de:0030-drops-34924},
  doi =		{10.4230/LIPIcs.RTA.2012.176},
  annote =	{Keywords: higher-order rewriting, termination, polynomial interpretations, weakly monotonic algebras, automation}
}
Document
DOI: 10.4230/DagSemProc.09411.4
Inductive Theorem Proving meets Dependency Pairs

Authors: Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs, and Peter Schneider-Kamp

Published in: Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010)

Abstract
Current techniques and tools for automated termination analysis of term rewrite systems (TRSs) are already very powerful. However, they fail for algorithms whose termination is essentially due to an inductive argument. Therefore, we show how to couple the dependency pair method for TRS termination with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are also successful on this important class of algorithms.
Cite as

Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs, and Peter Schneider-Kamp. Inductive Theorem Proving meets Dependency Pairs. In Interaction versus Automation: The two Faces of Deduction. Dagstuhl Seminar Proceedings, Volume 9411, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{swiderski_et_al:DagSemProc.09411.4,
  author =	{Swiderski, Stephan and Parting, Michael and Giesl, J\"{u}rgen and Fuhs, Carsten and Schneider-Kamp, Peter},
  title =	{{Inductive Theorem Proving meets Dependency Pairs}},
  booktitle =	{Interaction versus Automation: The two Faces of Deduction},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9411},
  editor =	{Thomas Ball and J\"{u}rgen Giesl and Reiner H\"{a}hnle and Tobias Nipkow},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09411.4},
  URN =		{urn:nbn:de:0030-drops-24220},
  doi =		{10.4230/DagSemProc.09411.4},
  annote =	{Keywords: Termination, Term Rewriting, Dependency Pairs, Inductive Theorem Proving}
}
Document
DOI: 10.4230/DagSemProc.09411.5
Termination of Integer Term Rewriting

Authors: Carsten Fuhs, Jürgen Giesl, Martin Plücker, Peter Schneider-Kamp, and Stephan Falke

Published in: Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010)

Abstract
Recently, techniques and tools from term rewriting have been successfully applied to prove termination automatically for different programming languages. The advantage of rewrite techniques is that they are very powerful for algorithms on user-defined data structures. But in contrast to techniques for termination analysis of imperative programs, the drawback of rewrite techniques is that they do not support data structures like integer numbers which are pre-defined in almost all programming languages. To solve this problem, we extend term rewriting by built-in integers and adapt the dependency pair framework to prove termination of integer term rewriting automatically. Our experiments show that this indeed combines the power of rewrite techniques on user-defined data types with a powerful treatment of pre-defined integers.
Cite as

Carsten Fuhs, Jürgen Giesl, Martin Plücker, Peter Schneider-Kamp, and Stephan Falke. Termination of Integer Term Rewriting. In Interaction versus Automation: The two Faces of Deduction. Dagstuhl Seminar Proceedings, Volume 9411, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{fuhs_et_al:DagSemProc.09411.5,
  author =	{Fuhs, Carsten and Giesl, J\"{u}rgen and Pl\"{u}cker, Martin and Schneider-Kamp, Peter and Falke, Stephan},
  title =	{{Termination of Integer Term Rewriting}},
  booktitle =	{Interaction versus Automation: The two Faces of Deduction},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9411},
  editor =	{Thomas Ball and J\"{u}rgen Giesl and Reiner H\"{a}hnle and Tobias Nipkow},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09411.5},
  URN =		{urn:nbn:de:0030-drops-24233},
  doi =		{10.4230/DagSemProc.09411.5},
  annote =	{Keywords: Termination analysis, integers, term rewriting, dependency pairs}
}
Document
DOI: 10.4230/DagSemProc.07401.5
Implementing RPO and POLO using SAT

Authors: Peter Schneider-Kamp, Carsten Fuhs, René Thiemann, Jürgen Giesl, Elena Annov, Michael Codish, Aart Middeldorp, and Harald Zankl

Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)

Abstract
Well-founded orderings are the most basic, but also most important ingredient to virtually all termination analyses. The recursive path order with status (RPO) and polynomial interpretations (POLO) are the two classes that are the most popular in the termination analysis of term rewrite systems. Numerous fully automated search algorithms for these classes have therefore been devised and implemented in termination tools. Unfortunately, the performance of these algorithms on all but the smallest termination problems has been lacking. E.g., recently developed transformations from programming languages like Haskell or Prolog allow to apply termination tools for term rewrite systems to real programming languages. The results of the transformations are often of non-trivial size, though, and cannot be handled efficiently by the existing algorithms. The need for more efficient search algorithms has triggered research in reducing these search problems into decision problems for which more efficient algorithms already exist. Here, we introduce an encoding of RPO and POLO to the satisfiability of propositional logic (SAT). We implemented these encodings in our termination tool AProVE. Extensive experiments have shown that one can obtain speedups in orders of magnitude by this encoding and the application of modern SAT solvers. The talk is based on joint work with Elena Annov, Mike Codish, Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, René Thiemann, and Harald Zankl.
Cite as

Peter Schneider-Kamp, Carsten Fuhs, René Thiemann, Jürgen Giesl, Elena Annov, Michael Codish, Aart Middeldorp, and Harald Zankl. Implementing RPO and POLO using SAT. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{schneiderkamp_et_al:DagSemProc.07401.5,
  author =	{Schneider-Kamp, Peter and Fuhs, Carsten and Thiemann, Ren\'{e} and Giesl, J\"{u}rgen and Annov, Elena and Codish, Michael and Middeldorp, Aart and Zankl, Harald},
  title =	{{Implementing RPO and POLO using SAT}},
  booktitle =	{Deduction and Decision Procedures},
  pages =	{1--10},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7401},
  editor =	{Franz Baader and Byron Cook and J\"{u}rgen Giesl and Robert Nieuwenhuis},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.5},
  URN =		{urn:nbn:de:0030-drops-12491},
  doi =		{10.4230/DagSemProc.07401.5},
  annote =	{Keywords: Termination, SAT, recursive path order, polynomial interpretation}
}
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