Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Franz Baader, Stefan Borgwardt, and Barbara Morawska. Dismatching and Local Disunification in EL. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 40-56, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{baader_et_al:LIPIcs.RTA.2015.40, author = {Baader, Franz and Borgwardt, Stefan and Morawska, Barbara}, title = {{Dismatching and Local Disunification in EL}}, booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)}, pages = {40--56}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.40}, URN = {urn:nbn:de:0030-drops-51884}, doi = {10.4230/LIPIcs.RTA.2015.40}, annote = {Keywords: Unification, Description Logics, SAT} }
Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)
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)
@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-dev.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} }
Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)
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)
@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-dev.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} }
Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)
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)
@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-dev.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} }
Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)
Silvio Ghilardi, Silvio Ranise, Enrica Nicolini, and Daniele Zucchelli. From Non-Disjoint Combination to Satisfiability and Model-Checking of Infinite State Systems. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)
@InProceedings{ghilardi_et_al:DagSemProc.07401.4, author = {Ghilardi, Silvio and Ranise, Silvio and Nicolini, Enrica and Zucchelli, Daniele}, title = {{From Non-Disjoint Combination to Satisfiability and Model-Checking of Infinite State Systems}}, booktitle = {Deduction and Decision Procedures}, pages = {1--2}, 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-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.4}, URN = {urn:nbn:de:0030-drops-12479}, doi = {10.4230/DagSemProc.07401.4}, annote = {Keywords: Non disjoint combination, linear temporal logic, model checking} }
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-dev.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} }
Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)
Viorica Sofronie-Stokkermans, Carsten Ihlemann, and Swen Jacobs. Local Theory Extensions, Hierarchical Reasoning and Applications to Verification. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)
@InProceedings{sofroniestokkermans_et_al:DagSemProc.07401.6, author = {Sofronie-Stokkermans, Viorica and Ihlemann, Carsten and Jacobs, Swen}, title = {{Local Theory Extensions, Hierarchical Reasoning and Applications to Verification}}, booktitle = {Deduction and Decision Procedures}, pages = {1--22}, 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-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.6}, URN = {urn:nbn:de:0030-drops-12507}, doi = {10.4230/DagSemProc.07401.6}, annote = {Keywords: Automated reasoning, Combinations of decision procedures, Verification} }
Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)
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)
@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-dev.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} }
Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)
Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, and Andrei Voronkov. 05431 Abstracts Collection – Deduction and Applications. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{baader_et_al:DagSemProc.05431.1, author = {Baader, Franz and Baumgartner, Peter and Nieuwenhuis, Robert and Voronkov, Andrei}, title = {{05431 Abstracts Collection – Deduction and Applications}}, booktitle = {Deduction and Applications}, pages = {1--23}, 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-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.1}, URN = {urn:nbn:de:0030-drops-5625}, doi = {10.4230/DagSemProc.05431.1}, annote = {Keywords: Formal logic, deduction, artificial intelligence} }
Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)
Jörg Siekmann. Proof Presentation. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{siekmann:DagSemProc.05431.5, author = {Siekmann, J\"{o}rg}, title = {{Proof Presentation}}, booktitle = {Deduction and Applications}, pages = {1--7}, 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-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.5}, URN = {urn:nbn:de:0030-drops-5611}, doi = {10.4230/DagSemProc.05431.5}, annote = {Keywords: Artificial intelligence, mathematics, proof presentation} }
Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)
Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, and Andrei Voronkov. 05431 Executive Summary – Deduction and Applications. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{baader_et_al:DagSemProc.05431.2, author = {Baader, Franz and Baumgartner, Peter and Nieuwenhuis, Robert and Voronkov, Andrei}, title = {{05431 Executive Summary – Deduction and Applications}}, booktitle = {Deduction and Applications}, pages = {1--3}, 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-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.2}, URN = {urn:nbn:de:0030-drops-5100}, doi = {10.4230/DagSemProc.05431.2}, annote = {Keywords: Formal logic, deduction, artificial intelligence} }
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-dev.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 Proceedings, Volume 5431, Deduction and Applications (2006)
Viktor Kuncak, Martin Rinard, and Bruno Marnette. On Algorithms and Complexity for Sets with Cardinality Constraints. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)
@InProceedings{kuncak_et_al:DagSemProc.05431.4, author = {Kuncak, Viktor and Rinard, Martin and Marnette, Bruno}, title = {{On Algorithms and Complexity for Sets with Cardinality Constraints}}, booktitle = {Deduction and Applications}, 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-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.4}, URN = {urn:nbn:de:0030-drops-5125}, doi = {10.4230/DagSemProc.05431.4}, annote = {Keywords: Static analysis, data structure consistency, program verification, decision procedures} }
Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)
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)
@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-dev.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} }
Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)
Franz Baader, Jörg Siekmann, and Wayne Snyder. 6th International Workshop on Unification (Dagstuhl Seminar 9231). Dagstuhl Seminar Report 42, pp. 1-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1992)
@TechReport{baader_et_al:DagSemRep.42, author = {Baader, Franz and Siekmann, J\"{o}rg and Snyder, Wayne}, title = {{6th International Workshop on Unification (Dagstuhl Seminar 9231)}}, pages = {1--32}, ISSN = {1619-0203}, year = {1992}, type = {Dagstuhl Seminar Report}, number = {42}, institution = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.42}, URN = {urn:nbn:de:0030-drops-149301}, doi = {10.4230/DagSemRep.42}, }
Feedback for Dagstuhl Publishing