RG1
Automation of Logic

Current Year

Bentkamp, A., Blanchette, J., Nummelin, V., Tourret, S., Vukmirović, P., & Waldmann, U. (2023). Mechanical Mathematicians. Communications of the ACM, 66(4). doi:10.1145/3557998
Export
BibTeX
@article{Bentkamp23b, TITLE = {Mechanical Mathematicians}, AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin and Nummelin, Visa and Tourret, Sophie and Vukmirovi{\'c}, Petar and Waldmann, Uwe}, LANGUAGE = {eng}, ISSN = {0001-0782}, DOI = {10.1145/3557998}, PUBLISHER = {ACM}, ADDRESS = {New York, NY}, YEAR = {2023}, MARGINALMARK = {$\bullet$}, JOURNAL = {Communications of the ACM}, VOLUME = {66}, NUMBER = {4}, PAGES = {80--90}, }
Endnote
%0 Journal Article %A Bentkamp, Alexander %A Blanchette, Jasmin %A Nummelin, Visa %A Tourret, Sophie %A Vukmirović, Petar %A Waldmann, Uwe %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Mechanical Mathematicians : %G eng %U http://hdl.handle.net/21.11116/0000-000D-06AE-9 %R 10.1145/3557998 %7 2023 %D 2023 %J Communications of the ACM %V 66 %N 4 %& 80 %P 80 - 90 %I ACM %C New York, NY %@ false
Bentkamp, A., Blanchette, J., Tourret, S., & Vukmirović, P. (2023). Superposition for Higher-Order Logic. Journal of Automated Reasoning, 67(1). doi:10.1007/s10817-022-09649-9
Export
BibTeX
@article{Bentkamp23, TITLE = {Superposition for Higher-Order Logic}, AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin and Tourret, Sophie and Vukmirovi{\'c}, Petar}, LANGUAGE = {eng}, ISSN = {0168-7433}, DOI = {10.1007/s10817-022-09649-9}, PUBLISHER = {D. Reidel Pub. Co.}, ADDRESS = {Dordrecht, Holland}, YEAR = {2023}, MARGINALMARK = {$\bullet$}, JOURNAL = {Journal of Automated Reasoning}, VOLUME = {67}, NUMBER = {1}, EID = {10}, }
Endnote
%0 Journal Article %A Bentkamp, Alexander %A Blanchette, Jasmin %A Tourret, Sophie %A Vukmirović, Petar %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Superposition for Higher-Order Logic : %G eng %U http://hdl.handle.net/21.11116/0000-000C-C5EB-D %R 10.1007/s10817-022-09649-9 %7 2023 %D 2023 %J Journal of Automated Reasoning %V 67 %N 1 %Z sequence number: 10 %I D. Reidel Pub. Co. %C Dordrecht, Holland %@ false
Blanchette, J., Qiu, Q., & Tourret, S. (2023). Given Clause Loops. Archive of Formal Proofs. Retrieved from https://isa-afp.org/entries/Given_Clause_Loops.html
Export
BibTeX
@article{Given_Clause_Loops-AFP, TITLE = {Given Clause Loops}, AUTHOR = {Blanchette, Jasmin and Qiu, Qi and Tourret, Sophie}, LANGUAGE = {eng}, ISSN = {2150-914x}, URL = {https://isa-afp.org/entries/Given_Clause_Loops.html}, PUBLISHER = {www.isa-afp.org}, YEAR = {2023}, MARGINALMARK = {$\bullet$}, JOURNAL = {Archive of Formal Proofs}, }
Endnote
%0 Journal Article %A Blanchette, Jasmin %A Qiu, Qi %A Tourret, Sophie %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Given Clause Loops : %G eng %U http://hdl.handle.net/21.11116/0000-000D-06C8-B %U https://isa-afp.org/entries/Given_Clause_Loops.html %7 2023 %D 2023 %J Archive of Formal Proofs %I www.isa-afp.org %@ false %U https://isa-afp.org/entries/Given_Clause_Loops.html
Bromberger, M., Schwarz, S., & Weidenbach, C. (2023). SCL(FOL) Revisited. Retrieved from https://arxiv.org/abs/2302.05954
(arXiv: 2302.05954)
Abstract
This paper presents an up-to-date and refined version of the SCL calculus for<br>first-order logic without equality. The refinement mainly consists of the<br>following two parts: First, we incorporate a stronger notion of regularity into<br>SCL(FOL). Our regularity definition is adapted from the SCL(T) calculus. This<br>adapted definition guarantees non-redundant clause learning during a run of<br>SCL. However, in contrast to the original presentation, it does not require<br>exhaustive propagation. Second, we introduce trail and model bounding to<br>achieve termination guarantees. In previous versions, no termination guarantees<br>about SCL were achieved. Last, we give rigorous proofs for soundness,<br>completeness and clause learning guarantees of SCL(FOL) and put SCL(FOL) into<br>context of existing first-order calculi.<br>
Export
BibTeX
@online{Bromberger_2302.05954, TITLE = {{SCL}({FOL}) Revisited}, AUTHOR = {Bromberger, Martin and Schwarz, Simon and Weidenbach, Christoph}, LANGUAGE = {eng}, URL = {https://arxiv.org/abs/2302.05954}, EPRINT = {2302.05954}, EPRINTTYPE = {arXiv}, YEAR = {2023}, MARGINALMARK = {$\bullet$}, ABSTRACT = {This paper presents an up-to-date and refined version of the SCL calculus for<br>first-order logic without equality. The refinement mainly consists of the<br>following two parts: First, we incorporate a stronger notion of regularity into<br>SCL(FOL). Our regularity definition is adapted from the SCL(T) calculus. This<br>adapted definition guarantees non-redundant clause learning during a run of<br>SCL. However, in contrast to the original presentation, it does not require<br>exhaustive propagation. Second, we introduce trail and model bounding to<br>achieve termination guarantees. In previous versions, no termination guarantees<br>about SCL were achieved. Last, we give rigorous proofs for soundness,<br>completeness and clause learning guarantees of SCL(FOL) and put SCL(FOL) into<br>context of existing first-order calculi.<br>}, }
Endnote
%0 Report %A Bromberger, Martin %A Schwarz, Simon %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T SCL(FOL) Revisited : %G eng %U http://hdl.handle.net/21.11116/0000-000C-C3B4-C %U https://arxiv.org/abs/2302.05954 %D 2023 %X This paper presents an up-to-date and refined version of the SCL calculus for<br>first-order logic without equality. The refinement mainly consists of the<br>following two parts: First, we incorporate a stronger notion of regularity into<br>SCL(FOL). Our regularity definition is adapted from the SCL(T) calculus. This<br>adapted definition guarantees non-redundant clause learning during a run of<br>SCL. However, in contrast to the original presentation, it does not require<br>exhaustive propagation. Second, we introduce trail and model bounding to<br>achieve termination guarantees. In previous versions, no termination guarantees<br>about SCL were achieved. Last, we give rigorous proofs for soundness,<br>completeness and clause learning guarantees of SCL(FOL) and put SCL(FOL) into<br>context of existing first-order calculi.<br> %K Computer Science, Logic in Computer Science, cs.LO,Computer Science, Symbolic Computation, cs.SC
Bromberger, M., Leutgeb, L., & Weidenbach, C. (2023). Explicit Model Construction for Saturated Constrained Horn Clauses. Retrieved from https://arxiv.org/abs/2305.05064
(arXiv: 2305.05064)
Abstract
Clause sets saturated by hierarchic superposition do not offer an explicit<br>model representation, rather the guarantee that all non-redundant inferences<br>have been performed without deriving a contradiction. We present an approach to<br>explicit model construction for saturated constrained Horn clauses. Constraints<br>are in linear arithmetic, the first-order part is restricted to a function-free<br>language. The model construction is effective and clauses can be evaluated with<br>respect to the model. Furthermore, we prove that our model construction<br>produces the least model.<br>
Export
BibTeX
@online{bromberger2023explicit, TITLE = {Explicit Model Construction for Saturated Constrained Horn Clauses}, AUTHOR = {Bromberger, Martin and Leutgeb, Lorenz and Weidenbach, Christoph}, LANGUAGE = {eng}, URL = {https://arxiv.org/abs/2305.05064}, EPRINT = {2305.05064}, EPRINTTYPE = {arXiv}, YEAR = {2023}, MARGINALMARK = {$\bullet$}, ABSTRACT = {Clause sets saturated by hierarchic superposition do not offer an explicit<br>model representation, rather the guarantee that all non-redundant inferences<br>have been performed without deriving a contradiction. We present an approach to<br>explicit model construction for saturated constrained Horn clauses. Constraints<br>are in linear arithmetic, the first-order part is restricted to a function-free<br>language. The model construction is effective and clauses can be evaluated with<br>respect to the model. Furthermore, we prove that our model construction<br>produces the least model.<br>}, }
Endnote
%0 Report %A Bromberger, Martin %A Leutgeb, Lorenz %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Explicit Model Construction for Saturated Constrained Horn Clauses : %G eng %U http://hdl.handle.net/21.11116/0000-000D-15DC-4 %U https://arxiv.org/abs/2305.05064 %D 2023 %X Clause sets saturated by hierarchic superposition do not offer an explicit<br>model representation, rather the guarantee that all non-redundant inferences<br>have been performed without deriving a contradiction. We present an approach to<br>explicit model construction for saturated constrained Horn clauses. Constraints<br>are in linear arithmetic, the first-order part is restricted to a function-free<br>language. The model construction is effective and clauses can be evaluated with<br>respect to the model. Furthermore, we prove that our model construction<br>produces the least model.<br> %K Computer Science, Logic in Computer Science, cs.LO
Ebner, G., Blanchette, J., & Tourret, S. (2023). Unifying Splitting. Journal of Automated Reasoning, 67(2). doi:10.1007/s10817-023-09660-8
Export
BibTeX
@article{Ebner23, TITLE = {Unifying Splitting}, AUTHOR = {Ebner, Gabriel and Blanchette, Jasmin and Tourret, Sophie}, LANGUAGE = {eng}, ISSN = {0168-7433}, DOI = {10.1007/s10817-023-09660-8}, PUBLISHER = {Springer}, ADDRESS = {New York, NY}, YEAR = {2023}, MARGINALMARK = {$\bullet$}, DATE = {2023}, JOURNAL = {Journal of Automated Reasoning}, VOLUME = {67}, NUMBER = {2}, PAGES = {1--44}, EID = {16}, }
Endnote
%0 Journal Article %A Ebner, Gabriel %A Blanchette, Jasmin %A Tourret, Sophie %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Unifying Splitting : %G eng %U http://hdl.handle.net/21.11116/0000-000D-2D8B-5 %R 10.1007/s10817-023-09660-8 %7 2023 %D 2023 %J Journal of Automated Reasoning %V 67 %N 2 %& 1 %P 1 - 44 %Z sequence number: 16 %I Springer %C New York, NY %@ false
Haifani, F. (2023). On a Notion of Abduction and Relevance for First-Order Logic Clause Sets. Universität des Saarlandes, Saarbrücken. Retrieved from urn:nbn:de:bsz:291--ds-393934
Export
BibTeX
@phdthesis{Haifani_PhD2023, TITLE = {On a Notion of Abduction and Relevance for First-Order Logic Clause Sets}, AUTHOR = {Haifani, Fajar}, LANGUAGE = {eng}, URL = {urn:nbn:de:bsz:291--ds-393934}, DOI = {10.22028/D291-39393}, SCHOOL = {Universit{\"a}t des Saarlandes}, ADDRESS = {Saarbr{\"u}cken}, YEAR = {2023}, MARGINALMARK = {$\bullet$}, }
Endnote
%0 Thesis %A Haifani, Fajar %Y Weidenbach, Christoph %A referee: Tourret, Sophie %A referee: Schulz, Stephan %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T On a Notion of Abduction and Relevance for First-Order Logic Clause Sets : %G eng %U http://hdl.handle.net/21.11116/0000-000C-FE92-1 %R 10.22028/D291-39393 %U urn:nbn:de:bsz:291--ds-393934 %F OTHER: hdl:20.500.11880/35608 %I Universit&#228;t des Saarlandes %C Saarbr&#252;cken %D 2023 %P xii,129 p. %V phd %9 phd %U https://scidok.sulb.uni-saarland.de/handle/20.500.11880/35608