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ät des Saarlandes
%C Saarbrücken
%D 2023
%P xii,129 p.
%V phd
%9 phd
%U https://scidok.sulb.uni-saarland.de/handle/20.500.11880/35608