Publications - Last 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.

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&#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.

mehr

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&#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.

mehr

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

Conference paper

RG1

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

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

mehr

BibTeX

@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

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.

mehr

BibTeX

@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.

mehr

BibTeX

@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.

mehr

BibTeX

@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
External Organizations
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.

mehr

BibTeX

@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

Paper

RG1

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

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

mehr

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.

mehr

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.

mehr

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

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.

mehr

BibTeX

@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.

mehr

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
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.

mehr

BibTeX

@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.

mehr

BibTeX

@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.

mehr

BibTeX

@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.

mehr

BibTeX

@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