Search Results

Documents authored by Giesl, Jürgen

Document
DOI: 10.4230/LIPIcs.FSCD.2024.16
On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems

Authors: Franz Baader and Jürgen Giesl

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Motivated by an application where we try to make proofs for Description Logic inferences smaller by rewriting, we consider the following decision problem, which we call the small term reachability problem: given a term rewriting system R, a term s, and a natural number n, decide whether there is a term t of size ≤ n reachable from s using the rules of R. We investigate the complexity of this problem depending on how termination of R can be established. We show that the problem is NP-complete for length-reducing term rewriting systems. Its complexity increases to N2ExpTime-complete (NExpTime-complete) if termination is proved using a (linear) polynomial order and to PSpace-complete for systems whose termination can be shown using a restricted class of Knuth-Bendix orders. Confluence reduces the complexity to P for the length-reducing case, but has no effect on the worst-case complexity in the other two cases.
Cite as

Franz Baader and Jürgen Giesl. On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{baader_et_al:LIPIcs.FSCD.2024.16,
  author =	{Baader, Franz and Giesl, J\"{u}rgen},
  title =	{{On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.16},
  URN =		{urn:nbn:de:0030-drops-203454},
  doi =		{10.4230/LIPIcs.FSCD.2024.16},
  annote =	{Keywords: Rewriting, Termination, Confluence, Creating small terms, Derivational complexity, Description Logics, Proof rewriting}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.334
Inferring Lower Bounds for Runtime Complexity

Authors: Florian Frohn, Jürgen Giesl, Jera Hensel, Cornelius Aschermann, and Thomas Ströder

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
We present the first approach to deduce lower bounds for innermost runtime complexity of term rewrite systems (TRSs) automatically. Inferring lower runtime bounds is useful to detect bugs and to complement existing techniques that compute upper complexity bounds. The key idea of our approach is to generate suitable families of rewrite sequences of a TRS and to find a relation between the length of such a rewrite sequence and the size of the first term in the sequence. We implemented our approach in the tool AProVE and evaluated it by extensive experiments.
Cite as

Florian Frohn, Jürgen Giesl, Jera Hensel, Cornelius Aschermann, and Thomas Ströder. Inferring Lower Bounds for Runtime Complexity. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 334-349, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{frohn_et_al:LIPIcs.RTA.2015.334,
  author =	{Frohn, Florian and Giesl, J\"{u}rgen and Hensel, Jera and Aschermann, Cornelius and Str\"{o}der, Thomas},
  title =	{{Inferring Lower Bounds for Runtime Complexity}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{334--349},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.334},
  URN =		{urn:nbn:de:0030-drops-52068},
  doi =		{10.4230/LIPIcs.RTA.2015.334},
  annote =	{Keywords: Term Rewriting, Runtime Complexity, Lower Bounds, Induction}
}
Document
DOI: 10.4230/LIPIcs.RTA.2011.155
Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting

Authors: Marc Brockschmidt, Carsten Otto, and Jürgen Giesl

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
In earlier work we presented an approach to prove termination of non-recursive Java Bytecode (JBC) programs automatically. Here, JBC programs are first transformed to finite termination graphs which represent all possible runs of the program. Afterwards, the termination graphs are translated to term rewrite systems (TRSs) such that termination of the resulting TRSs implies termination of the original JBC programs. So in this way, existing techniques and tools from term rewriting can be used to prove termination of JBC automatically. In this paper, we improve this approach substantially in two ways: (1) We extend it in order to also analyze recursive JBC programs. To this end, one has to represent call stacks of arbitrary size. (2) To handle JBC programs with several methods, we modularize our approach in order to re-use termination graphs and TRSs for the separate methods and to prove termination of the resulting TRS in a modular way. We implemented our approach in the tool AProVE. Our experiments show that the new contributions increase the power of termination analysis for JBC significantly.
Cite as

Marc Brockschmidt, Carsten Otto, and Jürgen Giesl. Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 155-170, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{brockschmidt_et_al:LIPIcs.RTA.2011.155,
  author =	{Brockschmidt, Marc and Otto, Carsten and Giesl, J\"{u}rgen},
  title =	{{Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{155--170},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.155},
  URN =		{urn:nbn:de:0030-drops-31146},
  doi =		{10.4230/LIPIcs.RTA.2011.155},
  annote =	{Keywords: termination, Java Bytecode, term rewriting, recursion}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.259
Automated Termination Analysis of Java Bytecode by Term Rewriting

Authors: Carsten Otto, Marc Brockschmidt, Christian von Essen, and Jürgen Giesl

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
We present an automated approach to prove termination of Java Bytecode (JBC) programs by automatically transforming them to term rewrite systems (TRSs). In this way, the numerous techniques and tools developed for TRS termination can now be used for imperative object-oriented languages like Java, which can be compiled into JBC.
Cite as

Carsten Otto, Marc Brockschmidt, Christian von Essen, and Jürgen Giesl. Automated Termination Analysis of Java Bytecode by Term Rewriting. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 259-276, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{otto_et_al:LIPIcs.RTA.2010.259,
  author =	{Otto, Carsten and Brockschmidt, Marc and von Essen, Christian and Giesl, J\"{u}rgen},
  title =	{{Automated Termination Analysis of Java Bytecode by Term Rewriting}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{259--276},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.259},
  URN =		{urn:nbn:de:0030-drops-26570},
  doi =		{10.4230/LIPIcs.RTA.2010.259},
  annote =	{Keywords: Java Bytecode, termination, term rewriting}
}
Document
DOI: 10.4230/DagSemProc.09411.1
09411 Abstracts Collection – Interaction versus Automation: The two Faces of Deduction

Authors: Thomas Ball, Jürgen Giesl, Reiner Hähnle, and Tobias Nipkow

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

Abstract
From 04.10. to 09.10.2009, the Dagstuhl Seminar 09411 ``Interaction versus Automation: The two Faces of Deduction'' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Thomas Ball, Jürgen Giesl, Reiner Hähnle, and Tobias Nipkow. 09411 Abstracts Collection – Interaction versus Automation: The two Faces of Deduction. In Interaction versus Automation: The two Faces of Deduction. Dagstuhl Seminar Proceedings, Volume 9411, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{ball_et_al:DagSemProc.09411.1,
  author =	{Ball, Thomas and Giesl, J\"{u}rgen and H\"{a}hnle, Reiner and Nipkow, Tobias},
  title =	{{09411 Abstracts Collection – Interaction versus Automation: The two Faces of Deduction}},
  booktitle =	{Interaction versus Automation: The two Faces of Deduction},
  pages =	{1--18},
  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.1},
  URN =		{urn:nbn:de:0030-drops-25032},
  doi =		{10.4230/DagSemProc.09411.1},
  annote =	{Keywords: Formal Logic, Deduction, Artificial Intelligence}
}
Document
DOI: 10.4230/DagSemProc.09411.2
09411 Executive Summary – Interaction versus Automation: The two Faces of Deductions

Authors: Thomas Ball, Jürgen Giesl, Reiner Hähnle, and Tobias Nipkow

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

Abstract
This seminar was the ninth in the series of the Dagstuhl "Deduction" seminars held biennially since 1993. Its goal was to bring together the closely related but unnecessarily disjoint communities of researchers working in interactive and automatic program verification.
Cite as

Thomas Ball, Jürgen Giesl, Reiner Hähnle, and Tobias Nipkow. 09411 Executive Summary – Interaction versus Automation: The two Faces of Deductions. 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{ball_et_al:DagSemProc.09411.2,
  author =	{Ball, Thomas and Giesl, J\"{u}rgen and H\"{a}hnle, Reiner and Nipkow, Tobias},
  title =	{{09411 Executive Summary – Interaction versus Automation: The two Faces of Deductions}},
  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.2},
  URN =		{urn:nbn:de:0030-drops-24213},
  doi =		{10.4230/DagSemProc.09411.2},
  annote =	{Keywords: Formal Logic, Deduction, Artificial Intelligence}
}
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.1
07401 Abstracts Collection – Deduction and Decision Procedures

Authors: Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis

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

Abstract
From 01.10. to 05.10.2007, the Dagstuhl Seminar 07401 ``Deduction and Decision Procedures'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper.
Cite as

Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis. 07401 Abstracts Collection – Deduction and Decision Procedures. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{baader_et_al:DagSemProc.07401.1,
  author =	{Baader, Franz and Cook, Byron and Giesl, J\"{u}rgen and Nieuwenhuis, Robert},
  title =	{{07401 Abstracts Collection – Deduction and Decision Procedures}},
  booktitle =	{Deduction and Decision Procedures},
  pages =	{1--20},
  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.1},
  URN =		{urn:nbn:de:0030-drops-12521},
  doi =		{10.4230/DagSemProc.07401.1},
  annote =	{Keywords: Decision Procedures, Deduction, Boolean Satisfiability, First-Order Logic, Integer Arithmetic, Combination of Theories, Satisfiability Modulo Theories Rewrite Systems, Formal Verification, Model Finding}
}
Document
DOI: 10.4230/DagSemProc.07401.2
07401 Executive Summary – Deduction and Decision Procedures

Authors: Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis

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

Abstract
Formal logic provides a mathematical foundation for many areas of computer science. Significant progress has been made in the challenge of making computers perform non-trivial logical reasoning. be it fully automatic, or in interaction with humans. In the last years it has become more and more evident that theory-specific reasoners, and in particular decision procedures, are extremely important in many applications of such deduction tools. General-purpose reasoning methods such as resolution or paramodulation alone are not efficient enough to handle the needs of real-world applications. % For this reason, the focus of this seminar was on decision procedures, their integration into general-purpose theorem provers, and the application of the integrated tools in computer science.
Cite as

Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis. 07401 Executive Summary – Deduction and Decision Procedures. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{baader_et_al:DagSemProc.07401.2,
  author =	{Baader, Franz and Cook, Byron and Giesl, J\"{u}rgen and Nieuwenhuis, Robert},
  title =	{{07401 Executive Summary – Deduction and Decision Procedures}},
  booktitle =	{Deduction and Decision Procedures},
  pages =	{1--3},
  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.2},
  URN =		{urn:nbn:de:0030-drops-12515},
  doi =		{10.4230/DagSemProc.07401.2},
  annote =	{Keywords: Formal Logic, Deduction, Artificial Intelligence}
}
Document
DOI: 10.4230/DagSemProc.07401.3
Decision Procedures for Loop Detection

Authors: René Thiemann, Jürgen Giesl, and Peter Schneider-Kamp

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

Abstract
The dependency pair technique is a powerful modular method for automated termination proofs of term rewrite systems. We first show that dependency pairs are also suitable for disproving termination: loops can be detected more easily. In a second step we analyze how to disprove innermost termination. Here, we present a novel procedure to decide whether a given loop is an innermost loop. All results have been implemented in the termination prover AProVE.
Cite as

René Thiemann, Jürgen Giesl, and Peter Schneider-Kamp. Decision Procedures for Loop Detection. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{thiemann_et_al:DagSemProc.07401.3,
  author =	{Thiemann, Ren\'{e} and Giesl, J\"{u}rgen and Schneider-Kamp, Peter},
  title =	{{Decision Procedures for Loop Detection}},
  booktitle =	{Deduction and Decision Procedures},
  pages =	{1--17},
  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.3},
  URN =		{urn:nbn:de:0030-drops-12469},
  doi =		{10.4230/DagSemProc.07401.3},
  annote =	{Keywords: Non-Termination, Decision Procedures, 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}
}
Document
DOI: 10.4230/DagSemProc.07401.7
Termination of Programs using Term Rewriting and SAT Solving

Authors: Jürgen Giesl, Peter Schneider-Kamp, René Thiemann, Stephan Swiderski, Manh Thang Nguyen, Daniel De Schreye, and Alexander Serebrenik

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

Abstract
There are many powerful techniques for automated termination analysis of term rewrite systems (TRSs). However, up to now they have hardly been used for real programming languages. In this talk, we describe recent results which permit the application of existing techniques from term rewriting in order to prove termination of programs. We discuss two possible approaches: 1. One could translate programs into TRSs and then use existing tools to verify termination of the resulting TRSs. 2. One could adapt TRS-techniques to the respective programming languages in order to analyze programs directly. We present such approaches for the functional language Haskell and the logic language Prolog. Our results have been implemented in the termination provers AProVE and Polytool. In order to handle termination problems resulting from real programs, these provers had to be coupled with modern SAT solvers, since the automation of the TRS-termination techniques had to improve significantly. Our resulting termination analyzers are currently the most powerful ones for Haskell and Prolog.
Cite as

Jürgen Giesl, Peter Schneider-Kamp, René Thiemann, Stephan Swiderski, Manh Thang Nguyen, Daniel De Schreye, and Alexander Serebrenik. Termination of Programs using Term Rewriting and SAT Solving. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{giesl_et_al:DagSemProc.07401.7,
  author =	{Giesl, J\"{u}rgen and Schneider-Kamp, Peter and Thiemann, Ren\'{e} and Swiderski, Stephan and Nguyen, Manh Thang and De Schreye, Daniel and Serebrenik, Alexander},
  title =	{{Termination of Programs using Term Rewriting and SAT Solving}},
  booktitle =	{Deduction and Decision Procedures},
  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.7},
  URN =		{urn:nbn:de:0030-drops-12481},
  doi =		{10.4230/DagSemProc.07401.7},
  annote =	{Keywords: Termination, Term Rewriting, Haskell, Prolog, SAT Solving}
}
Document
DOI: 10.4230/DagSemProc.05431.6
Proving and Disproving Termination in the Dependency Pair Framework

Authors: Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp

Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)

Abstract
The dependency pair framework is a new general concept to integrate arbitrary techniques for termination analysis of term rewriting. In this way, the benefits of different techniques can be combined and their modularity and power are increased significantly. Moreover, this framework facilitates the development of new methods for termination analysis. Traditionally, the research on termination focused on methods which prove termination and there were hardly any approaches for disproving termination. We show that with the dependency pair framework, one can combine the search for a proof and for a disproof of termination. In this way, we obtain the first powerful method which can also verify non-termination of term rewrite systems. We implemented and evaluated our contributions in the automated termination prover AProVE. Due to these results, AProVE was the winning tool in the International Competition of Termination Provers 2005, both for proving and for disproving termination of term rewriting.
Cite as

Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp. Proving and Disproving Termination in the Dependency Pair Framework. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{giesl_et_al:DagSemProc.05431.6,
  author =	{Giesl, J\"{u}rgen and Thiemann, Ren\'{e} and Schneider-Kamp, Peter},
  title =	{{Proving and Disproving Termination in the Dependency Pair Framework}},
  booktitle =	{Deduction and Applications},
  pages =	{1--1},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.6},
  URN =		{urn:nbn:de:0030-drops-5091},
  doi =		{10.4230/DagSemProc.05431.6},
  annote =	{Keywords: Termination, non-termination, term rewriting, dependency pairs}
}
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 About DROPS Imprint Privacy Contact