Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel. Seventeen Provers Under the Hammer. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{desharnais_et_al:LIPIcs.ITP.2022.8, author = {Desharnais, Martin and Vukmirovi\'{c}, Petar and Blanchette, Jasmin and Wenzel, Makarius}, title = {{Seventeen Provers Under the Hammer}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {8:1--8:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-252-5}, ISSN = {1868-8969}, year = {2022}, volume = {237}, editor = {Andronick, June and de Moura, Leonardo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.8}, URN = {urn:nbn:de:0030-drops-167178}, doi = {10.4230/LIPIcs.ITP.2022.8}, annote = {Keywords: Automatic theorem proving, interactive theorem proving, proof assistants} }
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} }
Feedback for Dagstuhl Publishing