Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Takahito Aoto, Naoki Nishida, and Jonas Schöpf. Equational Theories and Validity for Logically Constrained Term Rewriting. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{aoto_et_al:LIPIcs.FSCD.2024.31, author = {Aoto, Takahito and Nishida, Naoki and Sch\"{o}pf, Jonas}, title = {{Equational Theories and Validity for Logically Constrained Term Rewriting}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {31:1--31:21}, 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.31}, URN = {urn:nbn:de:0030-drops-203607}, doi = {10.4230/LIPIcs.FSCD.2024.31}, annote = {Keywords: constrained equation, constrained equational theory, logically constrained term rewriting, algebraic semantics, consistency} }
Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)
Raphael Douglas Giles, Vincent Jackson, and Christine Rizkallah. T-Rex: Termination of Recursive Functions Using Lexicographic Linear Combinations. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 139:1-139:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{giles_et_al:LIPIcs.ICALP.2024.139, author = {Giles, Raphael Douglas and Jackson, Vincent and Rizkallah, Christine}, title = {{T-Rex: Termination of Recursive Functions Using Lexicographic Linear Combinations}}, booktitle = {51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)}, pages = {139:1--139:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-322-5}, ISSN = {1868-8969}, year = {2024}, volume = {297}, editor = {Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.139}, URN = {urn:nbn:de:0030-drops-202827}, doi = {10.4230/LIPIcs.ICALP.2024.139}, annote = {Keywords: Termination, Recursive functions} }
Published in: LIPIcs, Volume 290, 27th International Conference on Database Theory (ICDT 2024)
Hubie Chen and Stefan Mengel. Optimally Rewriting Formulas and Database Queries: A Confluence of Term Rewriting, Structural Decomposition, and Complexity. In 27th International Conference on Database Theory (ICDT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 290, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{chen_et_al:LIPIcs.ICDT.2024.16, author = {Chen, Hubie and Mengel, Stefan}, title = {{Optimally Rewriting Formulas and Database Queries: A Confluence of Term Rewriting, Structural Decomposition, and Complexity}}, booktitle = {27th International Conference on Database Theory (ICDT 2024)}, pages = {16:1--16:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-312-6}, ISSN = {1868-8969}, year = {2024}, volume = {290}, editor = {Cormode, Graham and Shekelyan, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2024.16}, URN = {urn:nbn:de:0030-drops-197984}, doi = {10.4230/LIPIcs.ICDT.2024.16}, annote = {Keywords: width, query rewriting, structural decomposition, term rewriting} }
Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Cynthia Kop. WANDA - a Higher Order Termination Tool (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{kop:LIPIcs.FSCD.2020.36, author = {Kop, Cynthia}, title = {{WANDA - a Higher Order Termination Tool}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {36:1--36:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.36}, URN = {urn:nbn:de:0030-drops-123587}, doi = {10.4230/LIPIcs.FSCD.2020.36}, annote = {Keywords: higher-order term rewriting, termination, automatic analysis, dependency pair framework, higher-order recursive path ordering} }
Published in: Dagstuhl Reports, Volume 9, Issue 9 (2020)
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)
@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} }
Published in: Dagstuhl Reports, Volume 7, Issue 9 (2018)
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)
@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} }
Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)
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)
@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} }
Published in: Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010)
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)
@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} }
Published in: Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010)
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)
@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} }
Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)
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)
@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} }
Feedback for Dagstuhl Publishing