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 Reports, Volume 11, Issue 8 (2022)
Maria Paola Bonacina, Philipp Rümmer, and Renate A. Schmidt. Integrated Deduction (Dagstuhl Seminar 21371). In Dagstuhl Reports, Volume 11, Issue 8, pp. 35-51, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@Article{bonacina_et_al:DagRep.11.8.35, author = {Bonacina, Maria Paola and R\"{u}mmer, Philipp and Schmidt, Renate A.}, title = {{Integrated Deduction (Dagstuhl Seminar 21371)}}, pages = {35--51}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2022}, volume = {11}, number = {8}, editor = {Bonacina, Maria Paola and R\"{u}mmer, Philipp and Schmidt, Renate A.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.11.8.35}, URN = {urn:nbn:de:0030-drops-157685}, doi = {10.4230/DagRep.11.8.35}, annote = {Keywords: Automated theorem proving, deduction, logic, reasoning, SMT solving} }
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-dev.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} }
Feedback for Dagstuhl Publishing