Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
Florian Pollitt, Mathias Fleury, and Armin Biere. Faster LRAT Checking Than Solving with CaDiCaL. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 21:1-21:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{pollitt_et_al:LIPIcs.SAT.2023.21, author = {Pollitt, Florian and Fleury, Mathias and Biere, Armin}, title = {{Faster LRAT Checking Than Solving with CaDiCaL}}, booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)}, pages = {21:1--21:12}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-286-0}, ISSN = {1868-8969}, year = {2023}, volume = {271}, editor = {Mahajan, Meena and Slivovsky, Friedrich}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.21}, URN = {urn:nbn:de:0030-drops-184837}, doi = {10.4230/LIPIcs.SAT.2023.21}, annote = {Keywords: SAT solving, Proof Checking, DRAT, LRAT, FRAT} }
Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin. Efficient Full Higher-Order Unification. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{vukmirovic_et_al:LIPIcs.FSCD.2020.5, author = {Vukmirovi\'{c}, Petar and Bentkamp, Alexander and Nummelin, Visa}, title = {{Efficient Full Higher-Order Unification}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {5:1--5:17}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.5}, URN = {urn:nbn:de:0030-drops-123271}, doi = {10.4230/LIPIcs.FSCD.2020.5}, annote = {Keywords: unification, higher-order logic, theorem proving, term rewriting, indexing data structures} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, and Dierk Schleicher. The DPRM Theorem in Isabelle (Short Paper). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 33:1-33:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{bayer_et_al:LIPIcs.ITP.2019.33, author = {Bayer, Jonas and David, Marco and Pal, Abhik and Stock, Benedikt and Schleicher, Dierk}, title = {{The DPRM Theorem in Isabelle}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {33:1--33:7}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.33}, URN = {urn:nbn:de:0030-drops-110883}, doi = {10.4230/LIPIcs.ITP.2019.33}, annote = {Keywords: DPRM theorem, Hilbert’s tenth problem, Diophantine predicates, Register machines, Recursively enumerable sets, Isabelle, Formal verification} }
Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel. Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{blanchette_et_al:LIPIcs.FSCD.2017.11, author = {Blanchette, Jasmin Christian and Fleury, Mathias and Traytel, Dmitriy}, title = {{Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {11:1--11:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.11}, URN = {urn:nbn:de:0030-drops-77155}, doi = {10.4230/LIPIcs.FSCD.2017.11}, annote = {Keywords: Multisets, ordinals, proof assistants} }
Feedback for Dagstuhl Publishing