Publications - The Year Before Last

Proceedings

RG1

E. Ábrahám and T. Sturm

Eds., SC-Square 2023 : Satisfiability Checking and Symbolic Computation 2023. CEUR-WS, 2023.

@proceedings{SCSquare2023,
TITLE = {SC-Square 2023 : Satisfiability Checking and Symbolic Computation 2023},
EDITOR = {{\'A}brah{\'a}m, Erika and Sturm, Thomas},
LANGUAGE = {eng},
ISSN = {1613-0073},
URL = {urn:nbn:de:0074-3455-4},
PUBLISHER = {CEUR-WS},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
DATE = {2023},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {3455},
ADDRESS = {Troms{\o}, Norway},
}

Endnote

%0 Conference Proceedings
%E &#193;brah&#225;m, Erika
%E Sturm, Thomas
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T SC-Square 2023 : Satisfiability Checking and Symbolic Computation 2023 : Proceedings of the 8th SC-Square Workshop
co-located with the 48th International Symposium on Symbolic and Algebraic Computation (ISSAC 2023)
%G eng
%U http://hdl.handle.net/21.11116/0000-0010-41C6-5
%U urn:nbn:de:0074-3455-4
%I CEUR-WS
%D 2023
%B 8th SC-Square Workshop
%Z date of event: 2023-07-28 - 2023-07-28
%D 2023
%C Troms&#248;, Norway
%S CEUR Workshop Proceedings
%V 3455
%@ false

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, V. Nummelin, S. Tourret, and U. Waldmann

“Complete and Efficient Higher-Order Reasoning via Lambda-Superposition,” ACM SIGLOG News, vol. 10, no. 4, 2023.

@article{Bentkamp23,
TITLE = {Complete and Efficient Higher-Order Reasoning via Lambda-Superposition},
AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin and Nummelin, Visa and Tourret, Sophie and Waldmann, Uwe},
LANGUAGE = {eng},
DOI = {10.1145/3636362.3636367},
PUBLISHER = {ACM},
ADDRESS = {New York, NY},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
DATE = {2023},
JOURNAL = {ACM SIGLOG News},
VOLUME = {10},
NUMBER = {4},
PAGES = {25--40},
}

Endnote

%0 Journal Article
%A Bentkamp, Alexander
%A Blanchette, Jasmin
%A Nummelin, Visa
%A Tourret, Sophie
%A Waldmann, Uwe
%+ External Organizations
External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Complete and Efficient Higher-Order Reasoning via Lambda-Superposition : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0010-41AC-3
%R 10.1145/3636362.3636367
%7 2023-12-04
%D 2023
%J ACM SIGLOG News
%V 10
%N 4
%& 25
%P 25 - 40
%I ACM
%C New York, NY

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{Bentkamp23c,
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

Conference paper

RG1

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

“Verified Given Clause Procedures,” in Automated Deductions -- CADE 29, Rome, Italy, 2023.

@inproceedings{Blanchette_CADE23,
TITLE = {Verified Given Clause Procedures},
AUTHOR = {Blanchette, Jasmin and Qiu, Qi and Tourret, Sophie},
LANGUAGE = {eng},
ISBN = {978-3-031-38498-1},
DOI = {10.1007/978-3-031-38499-8_4},
PUBLISHER = {Springer},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
DATE = {2023},
BOOKTITLE = {Automated Deductions -- CADE 29},
EDITOR = {Pientka, Brigitte and Tinelli, Cesare},
PAGES = {61--77},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {14132},
ADDRESS = {Rome, Italy},
}

Endnote

%0 Conference Proceedings
%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 Verified Given Clause Procedures : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000E-7573-D
%R 10.1007/978-3-031-38499-8_4
%D 2023
%B 29th International Conference on Automated Deduction
%Z date of event: 2023-07-01 - 2023-07-04
%C Rome, Italy
%B Automated Deductions -- CADE 29
%E Pientka, Brigitte; Tinelli, Cesare
%P 61 - 77
%I Springer
%@ 978-3-031-38498-1
%B Lecture Notes in Artificial Intelligence
%N 14132

Article

RG1

J. Blanchette and P. Vukmirović

“SAT-Inspired Higher-Order Eliminations,” Logical Methods in Computer Science, vol. 19, no. 2, 2023.

@article{Blanchette2208.07775,
TITLE = {{SAT}-Inspired Higher-Order Eliminations},
AUTHOR = {Blanchette, Jasmin and Vukmirovi{\'c}, Petar},
LANGUAGE = {eng},
ISSN = {1860-5974},
DOI = {10.46298/lmcs-19(2:9)2023},
PUBLISHER = {Episciences},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
DATE = {2023},
JOURNAL = {Logical Methods in Computer Science},
VOLUME = {19},
NUMBER = {2},
PAGES = {1--23},
EID = {9},
}

Endnote

%0 Journal Article
%A Blanchette, Jasmin
%A Vukmirovi&#263;, Petar
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T SAT-Inspired Higher-Order Eliminations : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000B-653C-1
%R 10.46298/lmcs-19(2:9)2023
%7 2023
%D 2023
%J Logical Methods in Computer Science
%V 19
%N 2
%& 1
%P 1 - 23
%Z sequence number: 9
%I Episciences
%@ false

Conference paper

RG1

Y. Briefs, H. Leidinger, and C. Weidenbach

“KBO Constraint Solving Revisited,” in Frontiers of Combining Systems (FroCoS 2023), Prague, Czech Republic, 2023.

@inproceedings{Briefs_FROCOS23,
TITLE = {{KBO} Constraint Solving Revisited},
AUTHOR = {Briefs, Yasmine and Leidinger, Hendrik and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-031-43368-9},
DOI = {10.1007/978-3-031-43369-6_5},
PUBLISHER = {Springer},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
DATE = {2023},
BOOKTITLE = {Frontiers of Combining Systems (FroCoS 2023)},
EDITOR = {Sattler, Uli and Suda, Martin},
PAGES = {81--98},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {14279},
ADDRESS = {Prague, Czech Republic},
}

Endnote

%0 Conference Proceedings
%A Briefs, Yasmine
%A Leidinger, Hendrik
%A Weidenbach, Christoph
%+ External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T KBO Constraint Solving Revisited : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000E-7579-7
%R 10.1007/978-3-031-43369-6_5
%D 2023
%B 14th International Symposium on Frontiers of Combining Systems
%Z date of event: 2023-09-20 - 2023-09-22
%C Prague, Czech Republic
%B Frontiers of Combining Systems
%E Sattler, Uli; Suda, Martin
%P 81 - 98
%I Springer
%@ 978-3-031-43368-9
%B Lecture Notes in Artificial Intelligence
%N 14279

Conference paper

RG1

M. Bromberger, M. Desharnais, and C. Weidenbach

“An Isabelle/HOL Formalization of the SCL(FOL) Calculus,” in Automated Deductions -- CADE 29, Rome, Italy, 2023.

@inproceedings{Bromberger_CADE23,
TITLE = {An {I}sabelle/{HOL} Formalization of the {SCL}({FOL}) Calculus},
AUTHOR = {Bromberger, Martin and Desharnais, Martin and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-031-38498-1},
DOI = {10.1007/978-3-031-38499-8_7},
PUBLISHER = {Springer},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
DATE = {2023},
BOOKTITLE = {Automated Deductions -- CADE 29},
EDITOR = {Pientka, Brigitte and Tinelli, Cesare},
PAGES = {116--133},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {14132},
ADDRESS = {Rome, Italy},
}

Endnote

%0 Conference Proceedings
%A Bromberger, Martin
%A Desharnais, Martin
%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 An Isabelle/HOL Formalization of the SCL(FOL) Calculus : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000E-7591-A
%R 10.1007/978-3-031-38499-8_7
%D 2023
%B 29th International Conference on Automated Deduction
%Z date of event: 2023-07-01 - 2023-07-04
%C Rome, Italy
%B Automated Deductions -- CADE 29
%E Pientka, Brigitte; Tinelli, Cesare
%P 116 - 133
%I Springer
%@ 978-3-031-38498-1
%B Lecture Notes in Artificial Intelligence
%N 14132

Conference paper

RG1

M. Bromberger, C. Jain, and C. Weidenbach

“SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning,” in Automated Deductions -- CADE 29, Rome, Italy, 2023.

@inproceedings{Bromberger_CADE23b,
TITLE = {{SCL}({FOL}) Can Simulate Non-Redundant Superposition Clause Learning},
AUTHOR = {Bromberger, Martin and Jain, Chaahat and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-031-38498-1},
DOI = {10.1007/978-3-031-38499-8_8},
PUBLISHER = {Springer},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
DATE = {2023},
BOOKTITLE = {Automated Deductions -- CADE 29},
EDITOR = {Pientka, Brigitte and Tinelli, Cesare},
PAGES = {134--152},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {14132},
ADDRESS = {Rome, Italy},
}

Endnote

%0 Conference Proceedings
%A Bromberger, Martin
%A Jain, Chaahat
%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) Can Simulate Non-Redundant Superposition Clause Learning : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000E-7596-5
%R 10.1007/978-3-031-38499-8_8
%D 2023
%B 29th International Conference on Automated Deduction
%Z date of event: 2023-07-01 - 2023-07-04
%C Rome, Italy
%B Automated Deductions -- CADE 29
%E Pientka, Brigitte; Tinelli, Cesare
%P 134 - 152
%I Springer
%@ 978-3-031-38498-1
%B Lecture Notes in Artificial Intelligence
%N 14132

Conference paper

RG1

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

“Symbolic Model Construction for Saturated Constrained Horn Clauses,” in Frontiers of Combining Systems (FroCoS 2023), Prague, Czech Republic, 2023.

@inproceedings{Bromberger_FROCOS23,
TITLE = {Symbolic Model Construction for Saturated Constrained {H}orn Clauses},
AUTHOR = {Bromberger, Martin and Leutgeb, Lorenz and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-031-43368-9},
DOI = {10.1007/978-3-031-43369-6_8},
PUBLISHER = {Springer},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
DATE = {2023},
BOOKTITLE = {Frontiers of Combining Systems (FroCoS 2023)},
EDITOR = {Sattler, Uli and Suda, Martin},
PAGES = {137--155},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {14279},
ADDRESS = {Prague, Czech Republic},
}

Endnote

%0 Conference Proceedings
%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 Symbolic Model Construction for Saturated Constrained Horn Clauses : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000E-759B-0
%R 10.1007/978-3-031-43369-6_8
%D 2023
%B 14th International Symposium on Frontiers of Combining Systems
%Z date of event: 2023-09-20 - 2023-09-22
%C Prague, Czech Republic
%B Frontiers of Combining Systems
%E Sattler, Uli; Suda, Martin
%P 137 - 155
%I Springer
%@ 978-3-031-43368-9
%B Lecture Notes in Artificial Intelligence
%N 14279

Conference paper

RG1

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

“Exploring Partial Models with SCL,” in Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2023), Manizales, Colombia, 2023.

@inproceedings{BrombergerLPAR23,
TITLE = {Exploring Partial Models with {SCL}},
AUTHOR = {Bromberger, Martin and Schwarz, Simon and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {2040-557X},
DOI = {10.29007/8br1},
PUBLISHER = {EasyChair},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
DATE = {2023},
BOOKTITLE = {Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2023)},
EDITOR = {Piskac, Ruzica and Voronkov, Andrei},
PAGES = {48--72},
SERIES = {EasyChair Proceedings in Computing},
VOLUME = {94},
ADDRESS = {Manizales, Colombia},
}

Endnote

%0 Conference Proceedings
%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 Exploring Partial Models with SCL : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0010-3E78-3
%R 10.29007/8br1
%D 2023
%B 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
%Z date of event: 2023-06-04 - 2023-06-09
%C Manizales, Colombia
%B Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
%E Piskac, Ruzica; Voronkov, Andrei
%P 48 - 72
%I EasyChair
%B EasyChair Proceedings in Computing
%N 94
%@ false

Paper

RG1

M. Bromberger, C. Jain, and C. Weidenbach

“SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning,” 2023. [Online]. Available: https://arxiv.org/abs/2305.12926.

Abstract

We show that SCL(FOL) can simulate the derivation of non-redundant clauses by
superposition for first-order logic without equality. Superposition-based
reasoning is performed with respect to a fixed reduction ordering. The
completeness proof of superposition relies on the grounding of the clause set.
It builds a ground partial model according to the fixed ordering, where minimal
false ground instances of clauses then trigger non-redundant superposition
inferences. We define a respective strategy for the SCL calculus such that
clauses learned by SCL and superposition inferences coincide. From this
perspective the SCL calculus can be viewed as a generalization of the
superposition calculus.

BibTeX

@online{Bromberger2305.12926,
TITLE = {{SCL}({FOL}) Can Simulate Non-Redundant Superposition Clause Learning},
AUTHOR = {Bromberger, Martin and Jain, Chaahat and Weidenbach, Christoph},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/2305.12926},
EPRINT = {2305.12926},
EPRINTTYPE = {arXiv},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
ABSTRACT = {We show that SCL(FOL) can simulate the derivation of non-redundant clauses by<br>superposition for first-order logic without equality. Superposition-based<br>reasoning is performed with respect to a fixed reduction ordering. The<br>completeness proof of superposition relies on the grounding of the clause set.<br>It builds a ground partial model according to the fixed ordering, where minimal<br>false ground instances of clauses then trigger non-redundant superposition<br>inferences. We define a respective strategy for the SCL calculus such that<br>clauses learned by SCL and superposition inferences coincide. From this<br>perspective the SCL calculus can be viewed as a generalization of the<br>superposition calculus.<br>},
}

Endnote

%0 Report
%A Bromberger, Martin
%A Jain, Chaahat
%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) Can Simulate Non-Redundant Superposition Clause Learning : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0010-8A3E-E
%U https://arxiv.org/abs/2305.12926
%D 2023
%X   We show that SCL(FOL) can simulate the derivation of non-redundant clauses by<br>superposition for first-order logic without equality. Superposition-based<br>reasoning is performed with respect to a fixed reduction ordering. The<br>completeness proof of superposition relies on the grounding of the clause set.<br>It builds a ground partial model according to the fixed ordering, where minimal<br>false ground instances of clauses then trigger non-redundant superposition<br>inferences. We define a respective strategy for the SCL calculus such that<br>clauses learned by SCL and superposition inferences coincide. From this<br>perspective the SCL calculus can be viewed as a generalization of the<br>superposition calculus.<br>
%K Computer Science, Logic in Computer Science, cs.LO,Computer Science, Artificial Intelligence, cs.AI,Computer Science, Symbolic Computation, cs.SC

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

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

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{bromberger2023symbolic,
TITLE = {Symbolic Model Construction for Saturated Constrained Horn Clauses},
AUTHOR = {Bromberger, Martin and Leutgeb, Lorenz and Weidenbach, Christoph},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/2305.05064v2},
EPRINT = {2305.05064v2},
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 Symbolic 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.05064v2
%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

Conference paper

RG1

N. Faroß and S. Schwarz

“Gröbner Bases for Boolean Function Minimization,” in Satisfiability Checking and Symbolic Computation 2023 (SC-Sqaure 2023), Tromsø, Norway, 2023.

@inproceedings{FarossSC-Square23,
TITLE = {Gr{\"o}bner Bases for {B}oolean Function Minimization},
AUTHOR = {Faro{\ss}, Nicolas and Schwarz, Simon},
LANGUAGE = {eng},
ISSN = {1613-0073},
URL = {https://ceur-ws.org/Vol-3455/short4.pdf; urn:nbn:de:0074-3455-4},
PUBLISHER = {CEUR-WS},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
DATE = {2023},
BOOKTITLE = {Satisfiability Checking and Symbolic Computation 2023 (SC-Sqaure 2023)},
EDITOR = {{\'A}brah{\'a}m, Erika and Sturm, Thomas},
PAGES = {61--68},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {3455},
ADDRESS = {Troms{\o}, Norway},
}

Endnote

%0 Conference Proceedings
%A Faro&#223;, Nicolas
%A Schwarz, Simon
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Gr&#246;bner Bases for Boolean Function Minimization : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0010-8854-6
%U https://ceur-ws.org/Vol-3455/short4.pdf
%D 2023
%B 8th SC-Square Workshop
%Z date of event: 2023-07-28 - 2023-07-28
%C Troms&#248;, Norway
%B Satisfiability Checking and Symbolic Computation 2023
%E &#193;brah&#225;m, Erika; Sturm, Thomas
%P 61 - 68
%I CEUR-WS
%B CEUR Workshop Proceedings
%N 3455
%@ false

Conference paper

RG1

M. Fleury and P. Lammich

“A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper),” in Automated Deductions -- CADE 29, Rome, Italy, 2023.

@inproceedings{Fleury_CADE23,
TITLE = {A More Pragmatic {CDCL} for {IsaSAT} and Targetting {LLVM} (Short Paper)},
AUTHOR = {Fleury, Mathias and Lammich, Peter},
LANGUAGE = {eng},
ISBN = {978-3-031-38498-1},
DOI = {10.1007/978-3-031-38499-8_12},
PUBLISHER = {Springer},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
DATE = {2023},
BOOKTITLE = {Automated Deductions -- CADE 29},
EDITOR = {Pientka, Brigitte and Tinelli, Cesare},
PAGES = {207--219},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {14132},
ADDRESS = {Rome, Italy},
}

Endnote

%0 Conference Proceedings
%A Fleury, Mathias
%A Lammich, Peter
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper) : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000E-75A4-5
%R 10.1007/978-3-031-38499-8_12
%D 2023
%B 29th International Conference on Automated Deduction
%Z date of event: 2023-07-01 - 2023-07-04
%C Rome, Italy
%B Automated Deductions -- CADE 29
%E Pientka, Brigitte; Tinelli, Cesare
%P 207 - 219
%I Springer
%@ 978-3-031-38498-1
%B Lecture Notes in Artificial Intelligence
%N 14132

Thesis

RG1IMPR-CS

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
International Max Planck Research School, 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

M. Hark, F. Frohn, and J. Giesl

“Termination of Triangular Polynomial Loops,” Formal Methods in System Design, 2023.

@article{Hark2023,
TITLE = {Termination of Triangular Polynomial Loops},
AUTHOR = {Hark, Marcel and Frohn, Florian and Giesl, J{\"u}rgen},
LANGUAGE = {eng},
ISSN = {0925-9856},
DOI = {10.1007/s10703-023-00440-z},
PUBLISHER = {Springer},
ADDRESS = {New York, NY},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
JOURNAL = {Formal Methods in System Design},
}

Endnote

%0 Journal Article
%A Hark, Marcel
%A Frohn, Florian
%A Giesl, J&#252;rgen
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Termination of Triangular Polynomial Loops : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000E-369D-5
%R 10.1007/s10703-023-00440-z
%7 2023
%D 2023
%J Formal Methods in System Design
%I Springer
%C New York, NY
%@ false

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

Conference paper

RG1

S. Möhle

“An Abstract CNF-to-d-DNNF Compiler Based on Chronological CDCL,” in Frontiers of Combining Systems (FroCoS 2023), Prague, Czech Republic, 2023.

@inproceedings{MoehleFROCOS23,
TITLE = {An Abstract {CNF}-to-d-{DNNF} Compiler Based on Chronological {CDCL}},
AUTHOR = {M{\"o}hle, Sibylle},
LANGUAGE = {eng},
ISBN = {978-3-031-43368-9},
DOI = {10.1007/978-3-031-43369-6_11},
PUBLISHER = {Springer},
YEAR = {2023},
MARGINALMARK = {$\bullet$},
DATE = {2023},
BOOKTITLE = {Frontiers of Combining Systems (FroCoS 2023)},
EDITOR = {Sattler, Uli and Suda, Martin},
PAGES = {195--213},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {14279},
ADDRESS = {Prague, Czech Republic},
}

Endnote

%0 Conference Proceedings
%A M&#246;hle, Sibylle
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T An Abstract CNF-to-d-DNNF Compiler Based on Chronological CDCL : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000E-75E4-D
%R 10.1007/978-3-031-43369-6_11
%D 2023
%B 14th International Symposium on Frontiers of Combining Systems
%Z date of event: 2023-09-20 - 2023-09-22
%C Prague, Czech Republic
%B Frontiers of Combining Systems
%E Sattler, Uli; Suda, Martin
%P 195 - 213
%I Springer
%@ 978-3-031-43368-9
%B Lecture Notes in Artificial Intelligence
%N 14279

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