Publications - Current Year

Article

RG1

A. Bentkamp, J. Blanchette, V. Nummelin, S. Tourret, P. Vukmirović, and U. Waldmann

“Mechanical Mathematicians,” Communications of the ACM, vol. 66, no. 4, 2023.

@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&#263;, 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

Article

RG1

A. Bentkamp, J. Blanchette, S. Tourret, and P. Vukmirović

“Superposition for Higher-Order Logic,” Journal of Automated Reasoning, vol. 67, no. 1, 2023.

@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&#263;, 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

Article

RG1

J. Blanchette, Q. Qiu, and S. Tourret

“Given Clause Loops,” Archive of Formal Proofs, 2023.

@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

Paper

RG1

M. Bromberger, S. Schwarz, and C. Weidenbach

“SCL(FOL) Revisited,” 2023. [Online]. Available: https://arxiv.org/abs/2302.05954.

Abstract

This paper presents an up-to-date and refined version of the SCL calculus for
first-order logic without equality. The refinement mainly consists of the
following two parts: First, we incorporate a stronger notion of regularity into
SCL(FOL). Our regularity definition is adapted from the SCL(T) calculus. This
adapted definition guarantees non-redundant clause learning during a run of
SCL. However, in contrast to the original presentation, it does not require
exhaustive propagation. Second, we introduce trail and model bounding to
achieve termination guarantees. In previous versions, no termination guarantees
about SCL were achieved. Last, we give rigorous proofs for soundness,
completeness and clause learning guarantees of SCL(FOL) and put SCL(FOL) into
context of existing first-order calculi.

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

Paper

RG1

M. Bromberger, L. Leutgeb, and C. Weidenbach

“Explicit Model Construction for Saturated Constrained Horn Clauses,” 2023. [Online]. Available: https://arxiv.org/abs/2305.05064.

Abstract

Clause sets saturated by hierarchic superposition do not offer an explicit
model representation, rather the guarantee that all non-redundant inferences
have been performed without deriving a contradiction. We present an approach to
explicit model construction for saturated constrained Horn clauses. Constraints
are in linear arithmetic, the first-order part is restricted to a function-free
language. The model construction is effective and clauses can be evaluated with
respect to the model. Furthermore, we prove that our model construction
produces the least model.

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

Article

RG1

G. Ebner, J. Blanchette, and S. Tourret

“Unifying Splitting,” Journal of Automated Reasoning, vol. 67, no. 2, 2023.

@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

Thesis

RG1

F. Haifani

“On a Notion of Abduction and Relevance for First-Order Logic Clause Sets,” Universität des Saarlandes, Saarbrücken, 2023.

@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

Article

RG1

H. Leidinger and C. Weidenbach

“SCL(EQ): SCL for First-Order Logic with Equality,” Journal of Automated Reasoning, vol. 67, 2023.

@article{LeidingerJAR23,
TITLE = {{SCL(EQ)}: {SCL} for First-Order Logic with Equality},
AUTHOR = {Leidinger, Hendrik and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-023-09673-3},
PUBLISHER = {Springer},
ADDRESS = {New York, NY},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {67},
EID = {22},
}

Endnote

%0 Journal Article
%A Leidinger, Hendrik
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T SCL(EQ): SCL for First-Order Logic with Equality : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000D-938E-D
%R 10.1007/s10817-023-09673-3
%7 2023
%D 2023
%J Journal of Automated Reasoning
%V 67
%Z sequence number: 22
%I Springer
%C New York, NY
%@ false

Article

RG1

G. Sutcliffe and M. Desharnais

“The 11th IJCAR automated theorem proving system competition – CASC-J11,” AI Communications, vol. 36, no. 2, 2023.

@article{Sutcliffe23,
TITLE = {The 11th {IJCAR} automated theorem proving system competition -- {CASC}-J11},
AUTHOR = {Sutcliffe, Geoff and Desharnais, Martin},
LANGUAGE = {eng},
ISSN = {0921-7126},
DOI = {10.3233/AIC-220244},
PUBLISHER = {IOS},
ADDRESS = {Amsterdam, Netherlands},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
JOURNAL = {AI Communications},
VOLUME = {36},
NUMBER = {2},
PAGES = {73--91},
}

Endnote

%0 Journal Article
%A Sutcliffe, Geoff
%A Desharnais, Martin
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T The 11th IJCAR automated theorem proving system competition &#8211; CASC-J11 : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000D-5797-7
%R 10.3233/AIC-220244
%7 2023
%D 2023
%J AI Communications
%V 36
%N 2
%& 73
%P 73 - 91
%I IOS
%C Amsterdam, Netherlands
%@ false