Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
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)
@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} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
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)
@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} }
Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
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)
@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} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
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)
@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} }
Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)
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)
@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} }
Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)
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)
@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} }
Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)
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)
@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}, }
Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)
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)
@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}, }
Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)
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)
@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}, }
Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)
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)
@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}, }