10 Search Results for "Kapur, Deepak"

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.FSCD.2024.27
A Verified Algorithm for Deciding Pattern Completeness

Authors: René Thiemann and Akihisa Yamada

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

Abstract
Pattern completeness is the property that the left-hand sides of a functional program cover all cases w.r.t. pattern matching. In the context of term rewriting a related notion is quasi-reducibility, a prerequisite if one wants to perform ground confluence proofs by rewriting induction. In order to certify such confluence proofs, we develop a novel algorithm that decides pattern completeness and that can be used to ensure quasi-reducibility. One of the advantages of the proposed algorithm is its simple structure: it is similar to that of a regular matching algorithm and, unlike an existing decision procedure for quasi-reducibility, it avoids enumerating all terms up to a given depth. Despite the simple structure, proving the correctness of the algorithm is not immediate. Therefore we formalize the algorithm and verify its correctness using the proof assistant Isabelle/HOL. To this end, we not only verify some auxiliary algorithms, but also design an Isabelle library on sorted term rewriting. Moreover, we export the verified code in Haskell and experimentally evaluate its performance. We observe that our algorithm significantly outperforms existing algorithms, even including the pattern completeness check of the GHC Haskell compiler.
Cite as

René Thiemann and Akihisa Yamada. A Verified Algorithm for Deciding Pattern Completeness. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{thiemann_et_al:LIPIcs.FSCD.2024.27,
  author =	{Thiemann, Ren\'{e} and Yamada, Akihisa},
  title =	{{A Verified Algorithm for Deciding Pattern Completeness}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{27:1--27:17},
  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.27},
  URN =		{urn:nbn:de:0030-drops-203566},
  doi =		{10.4230/LIPIcs.FSCD.2024.27},
  annote =	{Keywords: Isabelle/HOL, pattern matching, term rewriting}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.15
A Modular Associative Commutative (AC) Congruence Closure Algorithm

Authors: Deepak Kapur

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
Algorithms for computing congruence closure of ground equations over uninterpreted symbols and interpreted symbols satisfying associativity and commutativity (AC) properties are proposed. The algorithms are based on a framework for computing the congruence closure by abstracting nonflat terms by constants as proposed first in Kapur’s congruence closure algorithm (RTA97). The framework is general, flexible, and has been extended also to develop congruence closure algorithms for the cases when associative-commutative function symbols can have additional properties including idempotency, nilpotency and/or have identities, as well as their various combinations. The algorithms are modular; their correctness and termination proofs are simple, exploiting modularity. Unlike earlier algorithms, the proposed algorithms neither rely on complex AC compatible well-founded orderings on nonvariable terms nor need to use the associative-commutative unification and extension rules in completion for generating canonical rewrite systems for congruence closures. They are particularly suited for integrating into Satisfiability modulo Theories (SMT) solvers.
Cite as

Deepak Kapur. A Modular Associative Commutative (AC) Congruence Closure Algorithm. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 15:1-15:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kapur:LIPIcs.FSCD.2021.15,
  author =	{Kapur, Deepak},
  title =	{{A Modular Associative Commutative (AC) Congruence Closure Algorithm}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{15:1--15:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.15},
  URN =		{urn:nbn:de:0030-drops-142530},
  doi =		{10.4230/LIPIcs.FSCD.2021.15},
  annote =	{Keywords: Congruence Closure, Associative and Commutative, Word Problems, Finitely Presented Algebras, Equational Theories}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2019.3
Extending Maximal Completion (Invited Talk)

Authors: Sarah Winkler

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
Maximal completion (Klein and Hirokawa 2011) is an elegantly simple yet powerful variant of Knuth-Bendix completion. This paper extends the approach to ordered completion and theorem proving as well as normalized completion. An implementation of the different procedures is described, and its practicality is demonstrated by various examples.
Cite as

Sarah Winkler. Extending Maximal Completion (Invited Talk). In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{winkler:LIPIcs.FSCD.2019.3,
  author =	{Winkler, Sarah},
  title =	{{Extending Maximal Completion}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{3:1--3:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.3},
  URN =		{urn:nbn:de:0030-drops-105102},
  doi =		{10.4230/LIPIcs.FSCD.2019.3},
  annote =	{Keywords: automated reasoning, completion, theorem proving}
}
Document
DOI: 10.4230/LIPIcs.RTA.2011.41
Termination Analysis of C Programs Using Compiler Intermediate Languages

Authors: Stephan Falke, Deepak Kapur, and Carsten Sinz

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

Abstract
Modeling the semantics of programming languages like C for the automated termination analysis of programs is a challenge if complete coverage of all language features should be achieved. On the other hand, low-level intermediate languages that occur during the compilation of C programs to machine code have a much simpler semantics since most of the intricacies of C are taken care of by the compiler frontend. It is thus a promising approach to use these intermediate languages for the automated termination analysis of C programs. In this paper we present the tool KITTeL based on this approach. For this, programs in the compiler intermediate language are translated into term rewrite systems (TRSs), and the termination proof itself is then performed on the automatically generated TRS. An evaluation on a large collection of C programs shows the effectiveness and practicality of KITTeL on "typical" examples.
Cite as

Stephan Falke, Deepak Kapur, and Carsten Sinz. Termination Analysis of C Programs Using Compiler Intermediate Languages. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 41-50, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{falke_et_al:LIPIcs.RTA.2011.41,
  author =	{Falke, Stephan and Kapur, Deepak and Sinz, Carsten},
  title =	{{Termination Analysis of C Programs Using Compiler Intermediate Languages}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{41--50},
  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.41},
  URN =		{urn:nbn:de:0030-drops-31232},
  doi =		{10.4230/LIPIcs.RTA.2011.41},
  annote =	{Keywords: termination analysis; C programs; compiler intermediate languages}
}
Document
DOI: 10.4230/DagSemProc.05431.3
Automatically Generating Loop Invariants Using Quantifier Elimination

Authors: Deepak Kapur

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

Abstract
An approach for automatically generating loop invariants using quantifier-elimination is proposed. An invariant of a loop is hypothesized as a parameterized formula. Parameters in the invariant are discovered by generating constraints on the parameters by ensuring that the formula is indeed preserved by the execution path corresponding to every basic cycle of the loop. The parameterized formula can be successively refined by considering execution paths one by one; heuristics can be developed for determining the order in which the paths are considered. Initialization of program variables as well as the precondition and postcondition of the loop, if available, can also be used to further refine the hypothesized invariant. Constraints on parameters generated in this way are solved for possible values of parameters. If no solution is possible, this means that an invariant of the hypothesized form does not exist for the loop. Otherwise, if the parametric constraints are solvable, then under certain conditions on methods for generating these constraints, the strongest possible invariant of the hypothesized form can be generated from most general solutions of the parametric constraints. The approach is illustrated using the first-order theory of polynomial equations as well as Presburger arithmetic.
Cite as

Deepak Kapur. Automatically Generating Loop Invariants Using Quantifier Elimination. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{kapur:DagSemProc.05431.3,
  author =	{Kapur, Deepak},
  title =	{{Automatically Generating Loop Invariants Using Quantifier Elimination}},
  booktitle =	{Deduction and Applications},
  pages =	{1--17},
  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.3},
  URN =		{urn:nbn:de:0030-drops-5116},
  doi =		{10.4230/DagSemProc.05431.3},
  annote =	{Keywords: Program verification, loop invariants, inductive assertions, quantifier elimination}
}
Document
DOI: 10.4230/DagSemRep.376
Deduction and Infinite-state Model Checking (Dagstuhl Seminar 03171)

Authors: Deepak Kapur, Andreas Podelski, and Andrei Voronkov

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Deepak Kapur, Andreas Podelski, and Andrei Voronkov. Deduction and Infinite-state Model Checking (Dagstuhl Seminar 03171). Dagstuhl Seminar Report 376, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2003)

Copy BibTex To Clipboard

@TechReport{kapur_et_al:DagSemRep.376,
  author =	{Kapur, Deepak and Podelski, Andreas and Voronkov, Andrei},
  title =	{{Deduction and Infinite-state Model Checking (Dagstuhl Seminar 03171)}},
  pages =	{1--5},
  ISSN =	{1619-0203},
  year =	{2003},
  type = 	{Dagstuhl Seminar Report},
  number =	{376},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.376},
  URN =		{urn:nbn:de:0030-drops-152564},
  doi =		{10.4230/DagSemRep.376},
}
Document
DOI: 10.4230/DagSemRep.300
Deduction (Dagstuhl Seminar 01101)

Authors: Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur. Deduction (Dagstuhl Seminar 01101). Dagstuhl Seminar Report 300, pp. 1-27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2001)

Copy BibTex To Clipboard

@TechReport{furbach_et_al:DagSemRep.300,
  author =	{Furbach, Ulrich and Ganzinger, Harald and Hasegawa, Ryuzo and Kapur, Deepak},
  title =	{{Deduction (Dagstuhl Seminar 01101)}},
  pages =	{1--27},
  ISSN =	{1619-0203},
  year =	{2001},
  type = 	{Dagstuhl Seminar Report},
  number =	{300},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.300},
  URN =		{urn:nbn:de:0030-drops-151843},
  doi =		{10.4230/DagSemRep.300},
}
Document
DOI: 10.4230/DagSemRep.232
Deduction (Dagstuhl Seminar 99091)

Authors: Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Ulrich Furbach, Harald Ganzinger, Ryuzo Hasegawa, and Deepak Kapur. Deduction (Dagstuhl Seminar 99091). Dagstuhl Seminar Report 232, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2000)

Copy BibTex To Clipboard

@TechReport{furbach_et_al:DagSemRep.232,
  author =	{Furbach, Ulrich and Ganzinger, Harald and Hasegawa, Ryuzo and Kapur, Deepak},
  title =	{{Deduction (Dagstuhl Seminar 99091)}},
  pages =	{1--24},
  ISSN =	{1619-0203},
  year =	{2000},
  type = 	{Dagstuhl Seminar Report},
  number =	{232},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.232},
  URN =		{urn:nbn:de:0030-drops-151182},
  doi =		{10.4230/DagSemRep.232},
}
Document
DOI: 10.4230/DagSemRep.122
Automation of Proof by Mathematical Induction (Dagstuhl Seminar 9530)

Authors: Alan Bundy, Robert S. Boyer, Deepak Kapur, and Christoph Walther

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Alan Bundy, Robert S. Boyer, Deepak Kapur, and Christoph Walther. Automation of Proof by Mathematical Induction (Dagstuhl Seminar 9530). Dagstuhl Seminar Report 122, pp. 1-40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1996)

Copy BibTex To Clipboard

@TechReport{bundy_et_al:DagSemRep.122,
  author =	{Bundy, Alan and Boyer, Robert S. and Kapur, Deepak and Walther, Christoph},
  title =	{{Automation of Proof by Mathematical Induction (Dagstuhl Seminar 9530)}},
  pages =	{1--40},
  ISSN =	{1619-0203},
  year =	{1996},
  type = 	{Dagstuhl Seminar Report},
  number =	{122},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.122},
  URN =		{urn:nbn:de:0030-drops-150107},
  doi =		{10.4230/DagSemRep.122},
}
  • Refine by Author
  • 7 Kapur, Deepak
  • 2 Furbach, Ulrich
  • 2 Ganzinger, Harald
  • 2 Hasegawa, Ryuzo
  • 1 Baader, Franz
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Automated reasoning
  • 1 Mathematics of computing
  • 1 Software and its engineering
  • 1 Theory of computation
  • 1 Theory of computation → Complexity theory and logic
  • Show More...

  • Refine by Keyword
  • 1 Associative and Commutative
  • 1 Confluence
  • 1 Congruence Closure
  • 1 Creating small terms
  • 1 Derivational complexity
  • Show More...

  • Refine by Type
  • 10 document

  • Refine by Publication Year
  • 2 2024
  • 1 1996
  • 1 2000
  • 1 2001
  • 1 2003
  • Show More...

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact