Publications - The Year Before Last

Article

RG1

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

“Superposition with Lambdas,” Journal of Automated Reasoning, vol. 65, 2021.

@article{Bentkamp21,
TITLE = {Superposition with Lambdas},
AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin and Tourret, Sophie and Vukmirovi{\'c}, Petar and Waldmann, Uwe},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-021-09595-y},
PUBLISHER = {Springer},
ADDRESS = {New York, NY},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {65},
PAGES = {893--940},
}

Endnote

%0 Journal Article
%A Bentkamp, Alexander
%A Blanchette, Jasmin
%A Tourret, Sophie
%A Vukmirovi&#263;, Petar
%A Waldmann, Uwe
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Superposition with Lambdas : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-2B35-C
%R 10.1007/s10817-021-09595-y
%7 2021
%D 2021
%J Journal of Automated Reasoning
%V 65
%& 893
%P 893 - 940
%I Springer
%C New York, NY
%@ false

Paper

RG1

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

“Superposition with Lambdas,” 2021. [Online]. Available: https://arxiv.org/abs/2102.00453.

Abstract

We designed a superposition calculus for a clausal fragment of extensional
polymorphic higher-order logic that includes anonymous functions but excludes
Booleans. The inference rules work on $\beta\eta$-equivalence classes of
$\lambda$-terms and rely on higher-order unification to achieve refutational
completeness. We implemented the calculus in the Zipperposition prover and
evaluated it on TPTP and Isabelle benchmarks. The results suggest that
superposition is a suitable basis for higher-order reasoning.

BibTeX

@online{Bentkamp2102.00453,
TITLE = {Superposition with Lambdas},
AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin and Tourret, Sophie and Vukmirovi{\'c}, Petar and Waldmann, Uwe},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/2102.00453},
EPRINT = {2102.00453},
EPRINTTYPE = {arXiv},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
ABSTRACT = {We designed a superposition calculus for a clausal fragment of extensional<br>polymorphic higher-order logic that includes anonymous functions but excludes<br>Booleans. The inference rules work on $\beta\eta$-equivalence classes of<br>$\lambda$-terms and rely on higher-order unification to achieve refutational<br>completeness. We implemented the calculus in the Zipperposition prover and<br>evaluated it on TPTP and Isabelle benchmarks. The results suggest that<br>superposition is a suitable basis for higher-order reasoning.<br>},
}

Endnote

%0 Report
%A Bentkamp, Alexander
%A Blanchette, Jasmin
%A Tourret, Sophie
%A Vukmirovi&#263;, Petar
%A Waldmann, Uwe
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Superposition with Lambdas : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0008-0A44-1
%U https://arxiv.org/abs/2102.00453
%D 2021
%X   We designed a superposition calculus for a clausal fragment of extensional<br>polymorphic higher-order logic that includes anonymous functions but excludes<br>Booleans. The inference rules work on $\beta\eta$-equivalence classes of<br>$\lambda$-terms and rely on higher-order unification to achieve refutational<br>completeness. We implemented the calculus in the Zipperposition prover and<br>evaluated it on TPTP and Isabelle benchmarks. The results suggest that<br>superposition is a suitable basis for higher-order reasoning.<br>
%K Computer Science, Logic in Computer Science, cs.LO,Computer Science, Artificial Intelligence, cs.AI

Article

RG1

A. Bentkamp, J. Blanchette, S. Cruanes, and U. Waldmann

“Superposition for Lambda-Free Higher-Order Logic,” Logical Methods in Computer Science, vol. 17, no. 2, 2021.

@article{Bentkamp2021,
TITLE = {Superposition for Lambda-Free Higher-Order Logic},
AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin and Cruanes, Simon and Waldmann, Uwe},
LANGUAGE = {eng},
DOI = {10.23638/LMCS-17(2:1)2021},
PUBLISHER = {https://lmcs.episciences.org},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
JOURNAL = {Logical Methods in Computer Science},
VOLUME = {17},
NUMBER = {2},
PAGES = {1--38},
EID = {1},
}

Endnote

%0 Journal Article
%A Bentkamp, Alexander
%A Blanchette, Jasmin
%A Cruanes, Simon
%A Waldmann, Uwe
%+ External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Superposition for Lambda-Free Higher-Order Logic : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-4AC7-4
%R 10.23638/LMCS-17(2:1)2021
%7 2021
%D 2021
%J Logical Methods in Computer Science
%V 17
%N 2
%& 1
%P 1 - 38
%Z sequence number: 1
%I https://lmcs.episciences.org

Conference paper

RG1

M. Bromberger, A. Fiori, and C. Weidenbach

“Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories,” in Verification, Model Checking, and Abstract Interpretation (VMCAI 2021), Copenhagen, Denmark (Online), 2021.

@inproceedings{BrombergerFioriWeidenbach_VMCAI2021,
TITLE = {Deciding the {Bernays}-{Schoenfinkel} Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories},
AUTHOR = {Bromberger, Martin and Fiori, Alberto and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-030-67066-5},
DOI = {10.1007/978-3-030-67067-2_23},
PUBLISHER = {Springer},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
BOOKTITLE = {Verification, Model Checking, and Abstract Interpretation (VMCAI 2021)},
EDITOR = {Henglein, Fritz and Shoham, Sharon and Yakir, Vizel},
PAGES = {511--533},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {12597},
ADDRESS = {Copenhagen, Denmark (Online)},
}

Endnote

%0 Conference Proceedings
%A Bromberger, Martin
%A Fiori, Alberto
%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 Deciding the Bernays-Schoenfinkel Fragment over Bounded 
Difference Constraints by Simple Clause Learning over Theories : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-7C49-D
%R 10.1007/978-3-030-67067-2_23
%D 2021
%B 22nd International Conference on Verification, Model Checking, and Abstract Interpretation
%Z date of event: 2021-01-17 - 2021-01-19
%C Copenhagen, Denmark (Online)
%B Verification, Model Checking, and Abstract Interpretation
%E Henglein, Fritz; Shoham, Sharon; Yakir, Vizel
%P 511 - 533
%I Springer
%@ 978-3-030-67066-5
%B Lecture Notes in Computer Science
%N 12597

Conference paper

RG1

M. Bromberger, I. Dragoste, R. Faqeh, C. Fetzer, M. Krötzsch, and C. Weidenbach

“A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic,” in Frontiers of Combining Systems (FroCoS 2021), Birmingham, UK, 2021.

@inproceedings{Bromberger_FroCoS,
TITLE = {A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic},
AUTHOR = {Bromberger, Martin and Dragoste, Irina and Faqeh, Rasha and Fetzer, Christof and Kr{\"o}tzsch, Markus and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-030-86204-6},
PUBLISHER = {Springer},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
BOOKTITLE = {Frontiers of Combining Systems (FroCoS 2021)},
EDITOR = {Konev, Boris and Reger, Giles},
PAGES = {3--24},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {12941},
ADDRESS = {Birmingham, UK},
}

Endnote

%0 Conference Proceedings
%A Bromberger, Martin
%A Dragoste, Irina
%A Faqeh, Rasha
%A Fetzer, Christof
%A Kr&#246;tzsch, Markus
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-4A0D-7
%D 2021
%B 13th International Symposium on Frontiers of Combining Systems 
%Z date of event: 2021-09-08 - 2021-09-10
%C Birmingham, UK
%B Frontiers of Combining Systems
%E Konev, Boris; Reger, Giles
%P 3 - 24
%I Springer
%@ 978-3-030-86204-6
%B Lecture Notes in Artificial Intelligence
%N 12941

Paper

RG1

M. Bromberger, I. Dragoste, R. Faqeh, C. Fetzer, M. Krötzsch, and C. Weidenbach

“A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic,” 2021. [Online]. Available: https://arxiv.org/abs/2107.03189.

Abstract

The Bernays-Sch\"onfinkel first-order logic fragment over simple linear real
arithmetic constraints BS(SLR) is known to be decidable. We prove that BS(SLR)
clause sets with both universally and existentially quantified verification
conditions (conjectures) can be translated into BS(SLR) clause sets over a
finite set of first-order constants. For the Horn case, we provide a Datalog
hammer preserving validity and satisfiability. A toolchain from the BS(LRA)
prover SPASS-SPL to the Datalog reasoner VLog establishes an effective way of
deciding verification conditions in the Horn fragment. This is exemplified by
the verification of supervisor code for a lane change assistant in a car and of
an electronic control unit for a supercharged combustion engine.

BibTeX

@online{Bromberger_2107.03189,
TITLE = {A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic},
AUTHOR = {Bromberger, Martin and Dragoste, Irina and Faqeh, Rasha and Fetzer, Christof and Kr{\"o}tzsch, Markus and Weidenbach, Christoph},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/2107.03189},
EPRINT = {2107.03189},
EPRINTTYPE = {arXiv},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
ABSTRACT = {The Bernays-Sch\"onfinkel first-order logic fragment over simple linear real<br>arithmetic constraints BS(SLR) is known to be decidable. We prove that BS(SLR)<br>clause sets with both universally and existentially quantified verification<br>conditions (conjectures) can be translated into BS(SLR) clause sets over a<br>finite set of first-order constants. For the Horn case, we provide a Datalog<br>hammer preserving validity and satisfiability. A toolchain from the BS(LRA)<br>prover SPASS-SPL to the Datalog reasoner VLog establishes an effective way of<br>deciding verification conditions in the Horn fragment. This is exemplified by<br>the verification of supervisor code for a lane change assistant in a car and of<br>an electronic control unit for a supercharged combustion engine.<br>},
}

Endnote

%0 Report
%A Bromberger, Martin
%A Dragoste, Irina
%A Faqeh, Rasha
%A Fetzer, Christof
%A Kr&#246;tzsch, Markus
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-4A01-3
%U https://arxiv.org/abs/2107.03189
%D 2021
%X   The Bernays-Sch\"onfinkel first-order logic fragment over simple linear real<br>arithmetic constraints BS(SLR) is known to be decidable. We prove that BS(SLR)<br>clause sets with both universally and existentially quantified verification<br>conditions (conjectures) can be translated into BS(SLR) clause sets over a<br>finite set of first-order constants. For the Horn case, we provide a Datalog<br>hammer preserving validity and satisfiability. A toolchain from the BS(LRA)<br>prover SPASS-SPL to the Datalog reasoner VLog establishes an effective way of<br>deciding verification conditions in the Horn fragment. This is exemplified by<br>the verification of supervisor code for a lane change assistant in a car and of<br>an electronic control unit for a supercharged combustion engine.<br>
%K Computer Science, Logic in Computer Science, cs.LO

Conference paper

RG1

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

“A Unifying Splitting Framework,” in Automated Deduction - CADE 28, Virtual Event, 2021.

@inproceedings{Ebner_CADE21,
TITLE = {A Unifying Splitting Framework},
AUTHOR = {Ebner, Gabriel and Blanchette, Jasmin and Tourret, Sophie},
LANGUAGE = {eng},
ISBN = {978-3-030-79875-8},
DOI = {10.1007/978-3-030-79876-5_20},
PUBLISHER = {Springer},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
BOOKTITLE = {Automated Deduction -- CADE 28},
EDITOR = {Platzer, Andr{\'e} and Sutcliffe, Geof},
PAGES = {344--360},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {12699},
ADDRESS = {Virtual Event},
}

Endnote

%0 Conference Proceedings
%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 A Unifying Splitting Framework : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-3F87-9
%R 10.1007/978-3-030-79876-5_20
%D 2021
%B 28th International Conference on Automated Deduction
%Z date of event: 2021-07-12 - 2021-07-15
%C Virtual Event
%B Automated Deduction - CADE 28
%E Platzer, Andr&#233;; Sutcliffe, Geof
%P 344 - 360
%I Springer
%@ 978-3-030-79875-8
%B Lecture Notes in Artificial Intelligence
%N 12699

Article

RG1

M. England, W. Koepf, T. Sadykov, W. M. Seiler, and T. Sturm

“Foreword, with a Dedication to Andreas Weber,” Mathematics in Computer Science, vol. 15, 2021.

@article{Eingland2020,
TITLE = {Foreword, with a Dedication to {Andreas Weber}},
AUTHOR = {England, Matthew and Koepf, Wolfram and Sadykov, Timor and Seiler, Werner M. and Sturm, Thomas},
LANGUAGE = {eng},
ISSN = {1661-8270},
DOI = {10.1007/s11786-020-00476-y},
PUBLISHER = {Springer},
ADDRESS = {New York, NY},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
JOURNAL = {Mathematics in Computer Science},
VOLUME = {15},
PAGES = {173--175},
}

Endnote

%0 Journal Article
%A England, Matthew
%A Koepf, Wolfram
%A Sadykov, Timor
%A Seiler, Werner M.
%A Sturm, Thomas
%+ External Organizations
External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Foreword, with a Dedication to Andreas Weber : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-79E1-3
%R 10.1007/s11786-020-00476-y
%7 2020
%D 2021
%J Mathematics in Computer Science
%V 15
%& 173
%P 173 - 175
%I Springer
%C New York, NY
%@ false
%U https://rdcu.be/cbpdy

Article

RG1

M. England, F. Boulier, T. Sadykov, and T. Sturm

“Foreword, with a Dedication to Vladimir Gerdt,” Mathematics in Computer Science, vol. 15, 2021.

@article{Boulier2021,
TITLE = {Foreword, with a Dedication to {Vladimir Gerdt}},
AUTHOR = {England, Matthew and Boulier, Fran{\c c}ois and Sadykov, Timor and Sturm, Thomas},
LANGUAGE = {eng},
ISSN = {1661-8270},
DOI = {10.1007/s11786-021-00509-0},
PUBLISHER = {Springer},
ADDRESS = {New York, NY},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
JOURNAL = {Mathematics in Computer Science},
VOLUME = {15},
PAGES = {369--371},
}

Endnote

%0 Journal Article
%A England, Matthew
%A Boulier, Fran&#231;ois
%A Sadykov, Timor
%A Sturm, Thomas
%+ External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Foreword, with a Dedication to Vladimir Gerdt : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-4B06-D
%R 10.1007/s11786-021-00509-0
%7 2021
%D 2021
%J Mathematics in Computer Science
%V 15
%& 369
%P 369 - 371
%I Springer
%C New York, NY
%@ false
%U https://rdcu.be/cyLbU

Conference paper

RG1

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

“Termination of Polynomial Loops,” in Static Analysis (SAS 2020), Chicago, IL, USA (Online Event), 2021.

@inproceedings{Frohn_SAS2020,
TITLE = {Termination of Polynomial Loops},
AUTHOR = {Frohn, Florian and Hark, Marcel and Giesl, J{\"u}rgen},
LANGUAGE = {eng},
ISBN = {978-3-030-65473-3},
DOI = {10.1007/978-3-030-65474-0_5},
PUBLISHER = {Springer},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2021},
BOOKTITLE = {Static Analysis (SAS 2020)},
EDITOR = {Pichardie, David and Sighireanu, Mihaela},
PAGES = {89--112},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {12389},
ADDRESS = {Chicago, IL, USA (Online Event)},
}

Endnote

%0 Conference Proceedings
%A Frohn, Florian
%A Hark, Marcel
%A Giesl, J&#252;rgen
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
%T Termination of Polynomial Loops : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-7FE3-B
%R 10.1007/978-3-030-65474-0_5
%D 2021
%B 27th International Static  Analysis Symposium
%Z date of event: 2020-11-18 - 2020-11-20
%C Chicago, IL, USA (Online Event)
%B Static Analysis
%E Pichardie, David; Sighireanu, Mihaela
%P 89 - 112
%I Springer
%@ 978-3-030-65473-3
%B Lecture Notes in Computer Science
%N 12389

Article

RG1

D. Grigoriev, A. Iosif, H. Rahkooy, T. Sturm, and A. Weber

“Efficiently and Effectively Recognizing Toricity of Steady State Varieties,” Mathematics in Computer Science, vol. 15, 2021.

@article{Grigoriev2020,
TITLE = {Efficiently and Effectively Recognizing Toricity of Steady State Varieties},
AUTHOR = {Grigoriev, Dima and Iosif, Alexandru and Rahkooy, Hamid and Sturm, Thomas and Weber, Andreas},
LANGUAGE = {eng},
ISSN = {1661-8270},
DOI = {10.1007/s11786-020-00479-9},
PUBLISHER = {Springer},
ADDRESS = {New York, NY},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
JOURNAL = {Mathematics in Computer Science},
VOLUME = {15},
PAGES = {199--232},
}

Endnote

%0 Journal Article
%A Grigoriev, Dima
%A Iosif, Alexandru
%A Rahkooy, Hamid
%A Sturm, Thomas
%A Weber, Andreas
%+ External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Efficiently and Effectively Recognizing Toricity of Steady State Varieties : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-79D1-5
%R 10.1007/s11786-020-00479-9
%7 2020
%D 2021
%J Mathematics in Computer Science
%V 15
%& 199
%P 199 - 232
%I Springer
%C New York, NY
%@ false
%U https://rdcu.be/cbpcc

Article

RG1

D. Grigoriev, A. Iosif, H. Rahkooy, T. Sturm, and A. Weber

“Efficiently and Effectively Recognizing Toricity of Steady State Varieties,” Mathematics in Computer Science, vol. 15, 2021.

@article{Grigoriev2021,
TITLE = {Efficiently and Effectively Recognizing Toricity of Steady State Varieties},
AUTHOR = {Grigoriev, Dima and Iosif, Alexandru and Rahkooy, Hamid and Sturm, Thomas and Weber, Andreas},
LANGUAGE = {eng},
DOI = {10.1007/s11786-020-00479-9},
PUBLISHER = {Springer},
ADDRESS = {New York, NY},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
JOURNAL = {Mathematics in Computer Science},
VOLUME = {15},
PAGES = {199--232},
}

Endnote

%0 Journal Article
%A Grigoriev, Dima
%A Iosif, Alexandru
%A Rahkooy, Hamid
%A Sturm, Thomas
%A Weber, Andreas
%+ External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Efficiently and Effectively Recognizing Toricity of Steady State Varieties : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-4AD0-9
%R 10.1007/s11786-020-00479-9
%7 2021
%D 2021
%J Mathematics in Computer Science
%V 15
%& 199
%P 199 - 232
%I Springer
%C New York, NY

Conference paper

RG1

F. Haifani, S. Tourret, and C. Weidenbach

“Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance,” in Automated Deduction - CADE 28, Virtual Event, 2021.

@inproceedings{Haifani_CADE21,
TITLE = {Generalized Completeness for {SOS} Resolution and its Application to a New Notion of Relevance},
AUTHOR = {Haifani, Fajar and Tourret, Sophie and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-030-79875-8},
DOI = {10.1007/978-3-030-79876-5_19},
PUBLISHER = {Springer},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
BOOKTITLE = {Automated Deduction -- CADE 28},
EDITOR = {Platzer, Andr{\'e} and Sutcliffe, Geof},
PAGES = {327--343},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {12699},
ADDRESS = {Virtual Event},
}

Endnote

%0 Conference Proceedings
%A Haifani, Fajar
%A Tourret, Sophie
%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 Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-3F8D-3
%R 10.1007/978-3-030-79876-5_19
%D 2021
%B 28th International Conference on Automated Deduction
%Z date of event: 2021-07-12 - 2021-07-15
%C Virtual Event
%B Automated Deduction - CADE 28
%E Platzer, Andr&#233;; Sutcliffe, Geof
%P 327 - 343
%I Springer
%@ 978-3-030-79875-8
%B Lecture Notes in Artificial Intelligence
%N 12699

Conference paper

RG1

F. Haifani, P. Koopmann, and S. Tourret

“Abduction in EL via Translation to FOL,” in Second-Order Quantifier Elimination and Related Topics (SOQE 2021), Online Event, 2021.

@inproceedings{Haifani_SOQE2021,
TITLE = {Abduction in {EL} via Translation to {FOL}},
AUTHOR = {Haifani, Fajar and Koopmann, Patrick and Tourret, Sophie},
LANGUAGE = {eng},
ISSN = {1613-0073},
URL = {urn:nbn:de:0074-3009-1},
PUBLISHER = {CEUR-WS},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
BOOKTITLE = {Second-Order Quantifier Elimination and Related Topics (SOQE 2021)},
EDITOR = {Schmidt, Renate A. and Wernhard, Christoph and Zhao, Yizheng},
PAGES = {46--58},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {3009},
ADDRESS = {Online Event},
}

Endnote

%0 Conference Proceedings
%A Haifani, Fajar
%A Koopmann, Patrick
%A Tourret, Sophie
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Abduction in EL via Translation to FOL : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000C-2152-2
%D 2021
%B Second Workshop on Second-Order Quantifier Elimination and Related Topics
%Z date of event: 2021-11-04 - 2021-11-04
%C Online Event
%B Second-Order Quantifier Elimination and Related Topics
%E Schmidt, Renate A.; Wernhard, Christoph; Zhao, Yizheng
%P 46 - 58
%I CEUR-WS
%B CEUR Workshop Proceedings
%N 3009
%@ false

Article

RG1

N. Kruff, C. Lüders, O. Radulescu, T. Sturm, and S. Walcher

“Algorithmic Reduction of Biological Networks With Multiple Time Scales,” Mathematics in Computer Science, vol. 15, 2021.

@article{Kruff2021,
TITLE = {Algorithmic Reduction of Biological Networks With Multiple Time Scales},
AUTHOR = {Kruff, Niclas and L{\"u}ders, Christoph and Radulescu, Ovidiu and Sturm, Thomas and Walcher, Sebastian},
LANGUAGE = {eng},
DOI = {10.1007/s11786-021-00515-2},
PUBLISHER = {Springer},
ADDRESS = {New York,NY},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
JOURNAL = {Mathematics in Computer Science},
VOLUME = {15},
PAGES = {499--534},
}

Endnote

%0 Journal Article
%A Kruff, Niclas
%A L&#252;ders, Christoph
%A Radulescu, Ovidiu
%A Sturm, Thomas
%A Walcher, Sebastian
%+ External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Algorithmic Reduction of Biological Networks With Multiple Time Scales : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-4B0A-9
%R 10.1007/s11786-021-00515-2
%7 2021
%D 2021
%J Mathematics in Computer Science
%V 15
%& 499
%P 499 - 534
%I Springer
%C New York,NY

Conference paper

RG1

V. Nummelin, A. Bentkamp, S. Tourret, and P. Vukmirović

“Superposition with First-class Booleans and Inprocessing Clausification,” in Automated Deduction - CADE 28, Virtual Event, 2021.

@inproceedings{Nummelin_CADE21,
TITLE = {Superposition with First-class {B}ooleans and Inprocessing Clausification},
AUTHOR = {Nummelin, Visa and Bentkamp, Alexander and Tourret, Sophie and Vukmirovi{\'c}, Petar},
LANGUAGE = {eng},
ISBN = {978-3-030-79875-8},
DOI = {10.1007/978-3-030-79876-5_22},
PUBLISHER = {Springer},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
BOOKTITLE = {Automated Deduction -- CADE 28},
EDITOR = {Platzer, Andr{\'e} and Sutcliffe, Geof},
PAGES = {378--395},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {12699},
ADDRESS = {Virtual Event},
}

Endnote

%0 Conference Proceedings
%A Nummelin, Visa
%A Bentkamp, Alexander
%A Tourret, Sophie
%A Vukmirovi&#263;, Petar
%+ External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Superposition with First-class Booleans and Inprocessing Clausification : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-3F95-9
%R 10.1007/978-3-030-79876-5_22
%D 2021
%B 28th International Conference on Automated Deduction
%Z date of event: 2021-07-12 - 2021-07-15
%C Virtual Event
%B Automated Deduction - CADE 28
%E Platzer, Andr&#233;; Sutcliffe, Geof
%P 378 - 395
%I Springer
%@ 978-3-030-79875-8
%B Lecture Notes in Artificial Intelligence
%N 12699

Conference paper

RG1

H. Rahkooy and C. Vargas Montero

“A Graph Theoretical Approach for Testing Binomiality of Reversible Chemical Reaction Networks,” in SYNASC 2020, 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, 2021.

@inproceedings{Rahkooy_SYNSAC20,
TITLE = {A Graph Theoretical Approach for Testing Binomiality of Reversible Chemical Reaction Networks},
AUTHOR = {Rahkooy, Hamid and Vargas Montero, Cristian},
LANGUAGE = {eng},
ISBN = {978-1-7281-7628-4},
DOI = {10.1109/SYNASC51798.2020.00027},
PUBLISHER = {IEEE},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
BOOKTITLE = {SYNASC 2020, 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing},
PAGES = {101--108},
ADDRESS = {Timisoara, Romania},
}

Endnote

%0 Conference Proceedings
%A Rahkooy, Hamid
%A Vargas Montero, Cristian
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T A Graph Theoretical Approach for Testing Binomiality of Reversible
  Chemical Reaction Networks : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-479F-5
%R 10.1109/SYNASC51798.2020.00027
%D 2021
%B 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
%Z date of event: 2020-09-01 - 2020-09-04
%C Timisoara, Romania
%B SYNASC 2020
%P 101 - 108
%I IEEE
%@ 978-1-7281-7628-4

Conference paper

RG1

H. Rahkooy and T. Sturm

“Parametric Toricity of Steady State Varieties of Reaction Networks,” in Computer Algebra in Scientific Computing (CASC 2021), Sochi, Russia, 2021.

@inproceedings{Rahkooy_CASC2021,
TITLE = {Parametric Toricity of Steady State Varieties of Reaction Networks},
AUTHOR = {Rahkooy, Hamid and Sturm, Thomas},
ISBN = {978-3-030-85164-4},
DOI = {10.1007/978-3-030-85165-1_18},
PUBLISHER = {Springer},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
BOOKTITLE = {Computer Algebra in Scientific Computing (CASC 2021)},
EDITOR = {Boulier, Fran{\c c}ois and England, Matthew and Sadykov, Timur M. and Vorozhtsov, Evgenii V.},
PAGES = {314--333},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {12865},
ADDRESS = {Sochi, Russia},
}

Endnote

%0 Conference Proceedings
%A Rahkooy, Hamid
%A Sturm, Thomas
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Parametric Toricity of Steady State Varieties of Reaction Networks : 
%U http://hdl.handle.net/21.11116/0000-0009-4B0D-6
%R 10.1007/978-3-030-85165-1_18
%D 2021
%B 23rd  International Workshop on Computer Algebra in Scienti&#64257;c Computing
%Z date of event: 2021-09-13 - 2021-09-17
%C Sochi, Russia
%B Computer Algebra in Scientific Computing
%E Boulier, Fran&#231;ois; England, Matthew; Sadykov, Timur M.; Vorozhtsov, Evgenii V.
%P 314 - 333
%I Springer
%@ 978-3-030-85164-4
%B Lecture Notes in Computer Science
%N 12865

Paper

RG1

H. Rahkooy and T. Sturm

“Parametric Toricity of Steady State Varieties of Reaction Networks,” 2021. [Online]. Available: https://arxiv.org/abs/2105.10853.

Abstract

We study real steady state varieties of the dynamics of chemical reaction
networks. The dynamics are derived using mass action kinetics with parametric
reaction rates. The models studied are not inherently parametric in nature.
Rather, our interest in parameters is motivated by parameter uncertainty, as
reaction rates are typically either measured with limited precision or
estimated. We aim at detecting toricity and shifted toricity, using a framework
that has been recently introduced and studied for the non-parametric case over
both the real and the complex numbers. While toricity requires that the variety
specifies a subgroup of the direct power of the multiplicative group of the
underlying field, shifted toricity requires only a coset. In the non-parametric
case these requirements establish real decision problems. In the presence of
parameters we must go further and derive necessary and sufficient conditions in
the parameters for toricity or shifted toricity to hold. Technically, we use
real quantifier elimination methods. Our computations on biological networks
here once more confirm shifted toricity as a relevant concept, while toricity
holds only for degenerate parameter choices.

BibTeX

@online{Rahkooy_arXiv2105.10853,
TITLE = {Parametric Toricity of Steady State Varieties of Reaction Networks},
AUTHOR = {Rahkooy, Hamid and Sturm, Thomas},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/2105.10853},
EPRINT = {2105.10853},
EPRINTTYPE = {arXiv},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
ABSTRACT = {We study real steady state varieties of the dynamics of chemical reaction<br>networks. The dynamics are derived using mass action kinetics with parametric<br>reaction rates. The models studied are not inherently parametric in nature.<br>Rather, our interest in parameters is motivated by parameter uncertainty, as<br>reaction rates are typically either measured with limited precision or<br>estimated. We aim at detecting toricity and shifted toricity, using a framework<br>that has been recently introduced and studied for the non-parametric case over<br>both the real and the complex numbers. While toricity requires that the variety<br>specifies a subgroup of the direct power of the multiplicative group of the<br>underlying field, shifted toricity requires only a coset. In the non-parametric<br>case these requirements establish real decision problems. In the presence of<br>parameters we must go further and derive necessary and sufficient conditions in<br>the parameters for toricity or shifted toricity to hold. Technically, we use<br>real quantifier elimination methods. Our computations on biological networks<br>here once more confirm shifted toricity as a relevant concept, while toricity<br>holds only for degenerate parameter choices.<br>},
}

Endnote

%0 Report
%A Rahkooy, Hamid
%A Sturm, Thomas
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Parametric Toricity of Steady State Varieties of Reaction Networks : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-4B11-0
%U https://arxiv.org/abs/2105.10853
%D 2021
%X   We study real steady state varieties of the dynamics of chemical reaction<br>networks. The dynamics are derived using mass action kinetics with parametric<br>reaction rates. The models studied are not inherently parametric in nature.<br>Rather, our interest in parameters is motivated by parameter uncertainty, as<br>reaction rates are typically either measured with limited precision or<br>estimated. We aim at detecting toricity and shifted toricity, using a framework<br>that has been recently introduced and studied for the non-parametric case over<br>both the real and the complex numbers. While toricity requires that the variety<br>specifies a subgroup of the direct power of the multiplicative group of the<br>underlying field, shifted toricity requires only a coset. In the non-parametric<br>case these requirements establish real decision problems. In the presence of<br>parameters we must go further and derive necessary and sufficient conditions in<br>the parameters for toricity or shifted toricity to hold. Technically, we use<br>real quantifier elimination methods. Our computations on biological networks<br>here once more confirm shifted toricity as a relevant concept, while toricity<br>holds only for degenerate parameter choices.<br>
%K Quantitative Biology, Molecular Networks, q-bio.MN,Computer Science, Logic in Computer Science, cs.LO,Computer Science, Symbolic Computation, cs.SC,

Paper

RG1

H. Rahkooy and T. Sturm

“Testing Binomiality of Chemical Reaction Networks Using Comprehensive Gröbner Systems,” 2021. [Online]. Available: https://arxiv.org/abs/2107.01706.

Abstract

We consider the problem of binomiality of the steady state ideals of
biochemical reaction networks. We are interested in finding polynomial
conditions on the parameters such that the steady state ideal of a chemical
reaction network is binomial under every specialisation of the parameters if
the conditions on the parameters hold. We approach the binomiality problem
using Comprehensive Gr\"obner systems. Considering rate constants as
parameters, we compute comprehensive Gr\"obner systems for various reactions.
In particular, we make automatic computations on n-site phosphorylations and
biomodels from the Biomodels repository using the grobcov library of the
computer algebra system Singular.

BibTeX

@online{Rahkooy_arXiv2107.01706,
TITLE = {Testing Binomiality of Chemical Reaction Networks Using Comprehensive Gr{\"o}bner Systems},
AUTHOR = {Rahkooy, Hamid and Sturm, Thomas},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/2107.01706},
EPRINT = {2107.01706},
EPRINTTYPE = {arXiv},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
ABSTRACT = {We consider the problem of binomiality of the steady state ideals of<br>biochemical reaction networks. We are interested in finding polynomial<br>conditions on the parameters such that the steady state ideal of a chemical<br>reaction network is binomial under every specialisation of the parameters if<br>the conditions on the parameters hold. We approach the binomiality problem<br>using Comprehensive Gr\"obner systems. Considering rate constants as<br>parameters, we compute comprehensive Gr\"obner systems for various reactions.<br>In particular, we make automatic computations on n-site phosphorylations and<br>biomodels from the Biomodels repository using the grobcov library of the<br>computer algebra system Singular.<br>},
}

Endnote

%0 Report
%A Rahkooy, Hamid
%A Sturm, Thomas
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Testing Binomiality of Chemical Reaction Networks Using Comprehensive Gr&#246;bner Systems : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-4B14-D
%U https://arxiv.org/abs/2107.01706
%D 2021
%X   We consider the problem of binomiality of the steady state ideals of<br>biochemical reaction networks. We are interested in finding polynomial<br>conditions on the parameters such that the steady state ideal of a chemical<br>reaction network is binomial under every specialisation of the parameters if<br>the conditions on the parameters hold. We approach the binomiality problem<br>using Comprehensive Gr\"obner systems. Considering rate constants as<br>parameters, we compute comprehensive Gr\"obner systems for various reactions.<br>In particular, we make automatic computations on n-site phosphorylations and<br>biomodels from the Biomodels repository using the grobcov library of the<br>computer algebra system Singular.<br>
%K Quantitative Biology, Molecular Networks, q-bio.MN,Computer Science, Symbolic Computation, cs.SC

Conference paper

RG1

H. Rahkooy and T. Sturm

“Testing Binomiality of Chemical Reaction Networks Using Comprehensive Gröbner Systems,” in Computer Algebra in Scientific Computing (CASC 2021), Sochi, Russia, 2021.

@inproceedings{Rahkooy_CASC2021b,
TITLE = {Testing Binomiality of Chemical Reaction Networks Using Comprehensive {G}r{\"o}bner Systems},
AUTHOR = {Rahkooy, Hamid and Sturm, Thomas},
ISBN = {978-3-030-85164-4},
DOI = {10.1007/978-3-030-85165-1_19},
PUBLISHER = {Springer},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
BOOKTITLE = {Computer Algebra in Scientific Computing (CASC 2021)},
EDITOR = {Boulier, Fran{\c c}ois and England, Matthew and Sadykov, Timur M. and Vorozhtsov, Evgenii V.},
PAGES = {334--352},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {12865},
ADDRESS = {Sochi, Russia},
}

Endnote

%0 Conference Proceedings
%A Rahkooy, Hamid
%A Sturm, Thomas
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Testing Binomiality of Chemical Reaction Networks Using Comprehensive Gr&#246;bner Systems : 
%U http://hdl.handle.net/21.11116/0000-0009-4B0F-4
%R 10.1007/978-3-030-85165-1_19
%D 2021
%B 23rd International Workshop on Computer Algebra in Scienti&#64257;c Computing
%Z date of event: 2021-09-13 - 2021-09-17
%C Sochi, Russia
%B Computer Algebra in Scientific Computing
%E Boulier, Fran&#231;ois; England, Matthew; Sadykov, Timur M.; Vorozhtsov, Evgenii V.
%P 334 - 352
%I Springer
%@ 978-3-030-85164-4
%B Lecture Notes in Computer Science
%N 12865

Conference paper

RG1

H.-J. Schurr, M. Fleury, and M. Desharnais

“Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant,” in Automated Deduction - CADE 28, Virtual Event, 2021.

@inproceedings{Schurr_CADE21,
TITLE = {Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant},
AUTHOR = {Schurr, Hans-J{\"o}rg and Fleury, Mathias and Desharnais, Martin},
LANGUAGE = {eng},
ISBN = {978-3-030-79875-8},
DOI = {10.1007/978-3-030-79876-5_26},
PUBLISHER = {Springer},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
BOOKTITLE = {Automated Deduction -- CADE 28},
EDITOR = {Platzer, Andr{\'e} and Sutcliffe, Geof},
PAGES = {450--467},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {12699},
ADDRESS = {Virtual Event},
}

Endnote

%0 Conference Proceedings
%A Schurr, Hans-J&#246;rg
%A Fleury, Mathias
%A Desharnais, Martin
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-3F9B-3
%R 10.1007/978-3-030-79876-5_26
%D 2021
%B 28th International Conference on Automated Deduction
%Z date of event: 2021-07-12 - 2021-07-15
%C Virtual Event
%B Automated Deduction - CADE 28
%E Platzer, Andr&#233;; Sutcliffe, Geof
%P 450 - 467
%I Springer
%@ 978-3-030-79875-8
%B Lecture Notes in Artificial Intelligence
%N 12699

Article

RG1

W. M. Seiler, M. Seiß, and T. Sturm

“A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations,” Mathematics in Computer Science, vol. 15, 2021.

@article{Seiler2020,
TITLE = {A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations},
AUTHOR = {Seiler, Werner M. and Sei{\ss}, Matthias and Sturm, Thomas},
LANGUAGE = {eng},
ISSN = {1661-8270},
DOI = {10.1007/s11786-020-00485-x},
PUBLISHER = {Springer},
ADDRESS = {New York, NY},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
JOURNAL = {Mathematics in Computer Science},
VOLUME = {15},
PAGES = {333--352},
}

Endnote

%0 Journal Article
%A Seiler, Werner M.
%A Sei&#223;, Matthias
%A Sturm, Thomas
%+ External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-79D5-1
%R 10.1007/s11786-020-00485-x
%7 2020
%D 2021
%J Mathematics in Computer Science
%V 15
%& 333
%P 333 - 352
%I Springer
%C New York, NY
%@ false
%U https://rdcu.be/cbpcP

Article

RG1

G. Sutcliffe and M. Desharnais

“The CADE-28 Automated Theorem Proving System Competition - CASC-28,” AI Communications, vol. 34, no. 4, 2021.

@article{Sutcliffe21,
TITLE = {The {CADE}-28 Automated Theorem Proving System Competition -- {CASC}-28},
AUTHOR = {Sutcliffe, Geoff and Desharnais, Martin},
LANGUAGE = {eng},
ISSN = {0921-7126},
DOI = {10.3233/AIC-210235},
PUBLISHER = {IOS},
ADDRESS = {Amsterdam, Netherlands},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
JOURNAL = {AI Communications},
VOLUME = {34},
NUMBER = {4},
PAGES = {259--276},
}

Endnote

%0 Journal Article
%A Sutcliffe, Geoff
%A Desharnais, Martin
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T The CADE-28 Automated Theorem Proving System Competition - CASC-28 : 
%G eng
%U http://hdl.handle.net/21.11116/0000-000A-3869-2
%R 10.3233/AIC-210235
%7 2021
%D 2021
%J AI Communications
%V 34
%N 4
%& 259
%P 259 - 276
%I IOS
%C Amsterdam, Netherlands
%@ false

Conference paper

RG1

S. Tourret and J. Blanchette

“A Modular Isabelle Framework for Verifying Saturation Provers,” in CPP ’21, 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual, Denmark, 2021.

@inproceedings{Tourret_CPP2021,
TITLE = {A modular {I}sabelle framework for verifying saturation provers},
AUTHOR = {Tourret, Sophie and Blanchette, Jasmin},
LANGUAGE = {eng},
ISBN = {978-1-4503-8299-1},
DOI = {10.1145/3437992.3439912},
PUBLISHER = {ACM},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
BOOKTITLE = {CPP '21, 10th ACM SIGPLAN International Conference on Certified Programs and Proofs},
EDITOR = {Hri{\c t}cu, C{\u a}t{\u a}lin and Popescu, Andrei},
PAGES = {224--237},
ADDRESS = {Virtual, Denmark},
}

Endnote

%0 Conference Proceedings
%A Tourret, Sophie
%A Blanchette, Jasmin
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T A Modular Isabelle Framework for Verifying Saturation Provers : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0008-0A0F-E
%R 10.1145/3437992.3439912
%D 2021
%B 10th ACM SIGPLAN International Conference on Certified Programs and Proofs
%Z date of event: 2021-01-17 - 2021-01-19
%C Virtual, Denmark
%B CPP '21
%E Hri&#355;cu, C&#259;t&#259;lin; Popescu, Andrei
%P 224 - 237
%I ACM
%@ 978-1-4503-8299-1

Article

RG1

M. Voigt

“Decidable ∃∗∀∗ First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates,” Journal of Automated Reasoning, vol. 65, 2021.

@article{Voigt2020,
TITLE = {Decidable ${\exists }^*{\forall }^*$ First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates},
AUTHOR = {Voigt, Marco},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-020-09567-8},
PUBLISHER = {Springer},
ADDRESS = {New York, NY},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {65},
PAGES = {357--423},
}

Endnote

%0 Journal Article
%A Voigt, Marco
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T Decidable &#8707;&#8727;&#8704;&#8727; First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0006-DC7C-8
%R 10.1007/s10817-020-09567-8
%7 2020
%D 2021
%J Journal of Automated Reasoning
%V 65
%& 357
%P 357 - 423
%I Springer
%C New York, NY
%@ false

Conference paper

RG1

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

“Making Higher-Order Superposition Work,” in Automated Deduction - CADE 28, Virtual Event, 2021.

@inproceedings{Vukmirovic_CADE21,
TITLE = {Making Higher-Order Superposition Work},
AUTHOR = {Vukmirovi{\'c}, Petar and Bentkamp, Alexander and Blanchette, Jasmin and Cruanes, Simon and Nummelin, Visa and Tourret, Sophie},
LANGUAGE = {eng},
ISBN = {978-3-030-79875-8},
DOI = {10.1007/978-3-030-79876-5_24},
PUBLISHER = {Springer},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
BOOKTITLE = {Automated Deduction -- CADE 28},
EDITOR = {Platzer, Andr{\'e} and Sutcliffe, Geof},
PAGES = {415--432},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {12699},
ADDRESS = {Virtual Event},
}

Endnote

%0 Conference Proceedings
%A Vukmirovi&#263;, Petar
%A Bentkamp, Alexander
%A Blanchette, Jasmin
%A Cruanes, Simon
%A Nummelin, Visa
%A Tourret, Sophie
%+ External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Making Higher-Order Superposition Work : 
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-3FA2-A
%R 10.1007/978-3-030-79876-5_24
%D 2021
%B 28th International Conference on Automated Deduction
%Z date of event: 2021-07-12 - 2021-07-15
%C Virtual Event
%B Automated Deduction - CADE 28
%E Platzer, Andr&#233;; Sutcliffe, Geof
%P 415 - 432
%I Springer
%@ 978-3-030-79875-8
%B Lecture Notes in Artificial Intelligence
%N 12699