Martin Desharnais, Balazs Toth. IsaFoL/Superposition_Calculus (Artifact, Isabelle/HOL theory files). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@misc{dagstuhl-artifact-22462, title = {{IsaFoL/Superposition\underlineCalculus}}, author = {Desharnais, Martin and Toth, Balazs}, note = {Other, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:9afd6985e81383a79df5325b0ea04e4fdc528228;origin=https://github.com/IsaFoL/IsaFoL;visit=swh:1:snp:3e98452c15e152e9c9dfef449a9116ac94cdeed5;anchor=swh:1:rev:a384a0f3b7e4207777cc4272daddffbd87cb7cc4}{\texttt{swh:1:dir:9afd6985e81383a79df5325b0ea04e4fdc528228}} (visited on 2024-11-28)}, url = {https://github.com/IsaFoL/IsaFoL/tree/ITP2024-IsaSuperposition/Superposition_Calculus}, doi = {10.4230/artifacts.22462}, }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette, and Sophie Tourret. A Modular Formalization of Superposition in Isabelle/HOL. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{desharnais_et_al:LIPIcs.ITP.2024.12, author = {Desharnais, Martin and Toth, Balazs and Waldmann, Uwe and Blanchette, Jasmin and Tourret, Sophie}, title = {{A Modular Formalization of Superposition in Isabelle/HOL}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {12:1--12:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.12}, URN = {urn:nbn:de:0030-drops-207401}, doi = {10.4230/LIPIcs.ITP.2024.12}, annote = {Keywords: Superposition, verification, first-order logic, higher-order logic} }
Published in: Dagstuhl Reports, Volume 13, Issue 11 (2024)
Maria Paola Bonacina, Pascal Fontaine, Cláudia Nalon, Claudia Schon, and Martin Desharnais. The Next Generation of Deduction Systems: From Composition to Compositionality (Dagstuhl Seminar 23471). In Dagstuhl Reports, Volume 13, Issue 11, pp. 130-150, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@Article{bonacina_et_al:DagRep.13.11.130, author = {Bonacina, Maria Paola and Fontaine, Pascal and Nalon, Cl\'{a}udia and Schon, Claudia and Desharnais, Martin}, title = {{The Next Generation of Deduction Systems: From Composition to Compositionality (Dagstuhl Seminar 23471)}}, pages = {130--150}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2024}, volume = {13}, number = {11}, editor = {Bonacina, Maria Paola and Fontaine, Pascal and Nalon, Cl\'{a}udia and Schon, Claudia and Desharnais, Martin}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.11.130}, URN = {urn:nbn:de:0030-drops-198472}, doi = {10.4230/DagRep.13.11.130}, annote = {Keywords: artificial intelligence, automated reasoning, compositionality, deduction, logic} }
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.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} }
Feedback for Dagstuhl Publishing