Current Year
Bentkamp, A., Blanchette, J. C., Tourret, S., Vukmirović, P., & Waldmann, U. (2021a). Superposition with Lambdas. Retrieved from https://arxiv.org/abs/2102.00453
(arXiv: 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.
Export
BibTeX
@online{Bentkamp2102.00453,
TITLE = {Superposition with Lambdas},
AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin Christian 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 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.},
}
Endnote
%0 Report
%A Bentkamp, Alexander
%A Blanchette, Jasmin Christian
%A Tourret, Sophie
%A Vukmirović, 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
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.
%K Computer Science, Logic in Computer Science, cs.LO,Computer Science, Artificial Intelligence, cs.AI
Bentkamp, A., Blanchette, J. C., Tourret, S., Vukmirović, P., & Waldmann, U. (2021b). Superposition with Lambdas. Journal of Automated Reasoning, 65. doi:10.1007/s10817-021-09595-y
Export
BibTeX
@article{Bentkamp21,
TITLE = {Superposition with Lambdas},
AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin Christian 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 Christian
%A Tourret, Sophie
%A Vukmirović, 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
Bentkamp, A., Blanchette, J. C., Cruanes, S., & Waldmann, U. (2021a). Superposition for Full Higher-order Logic. In Automated Deduction - CADE 28. Virtual Event: Springer. doi:10.1007/978-3-030-79876-5_23
Export
BibTeX
@inproceedings{Bentkamp_CADE21,
TITLE = {Superposition for Full Higher-order Logic},
AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin Christian and Cruanes, Simon and Waldmann, Uwe},
LANGUAGE = {eng},
ISBN = {978-3-030-79875-8},
DOI = {10.1007/978-3-030-79876-5_23},
PUBLISHER = {Springer},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
DATE = {2021},
BOOKTITLE = {Automated Deduction -- CADE 28},
EDITOR = {Platzer, Andr{\'e} and Sutcliffe, Geof},
PAGES = {396--412},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {12699},
ADDRESS = {Virtual Event},
}
Endnote
%0 Conference Proceedings
%A Bentkamp, Alexander
%A Blanchette, Jasmin Christian
%A Cruanes, Simon
%A Waldmann, Uwe
%+ External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Superposition for Full Higher-order Logic :
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-3F7F-4
%R 10.1007/978-3-030-79876-5_23
%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é; Sutcliffe, Geof
%P 396 - 412
%I Springer
%@ 978-3-030-79875-8
%B Lecture Notes in Artificial Intelligence
%N 12699
Bentkamp, A., Blanchette, J. C., Cruanes, S., & Waldmann, U. (2021b). Superposition for Lambda-Free Higher-Order Logic. Logical Methods in Computer Science, 17(2). doi:10.23638/LMCS-17(2:1)2021
Export
BibTeX
@article{Bentkamp2021,
TITLE = {Superposition for Lambda-Free Higher-Order Logic},
AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin Christian 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 Christian
%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
Bromberger, M., Fiori, A., & Weidenbach, C. (2021). 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): Springer. doi:10.1007/978-3-030-67067-2_23
Export
BibTeX
@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
Bromberger, M., Dragoste, I., Faqeh, R., Fetzer, C., Krötzsch, M., & Weidenbach, C. (2021a). A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. Retrieved from https://arxiv.org/abs/2107.03189
(arXiv: 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.
Export
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 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.},
}
Endnote
%0 Report
%A Bromberger, Martin
%A Dragoste, Irina
%A Faqeh, Rasha
%A Fetzer, Christof
%A Krö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
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.
%K Computer Science, Logic in Computer Science, cs.LO
Bromberger, M., Dragoste, I., Faqeh, R., Fetzer, C., Krötzsch, M., & Weidenbach, C. (2021b). A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic. In Frontiers of Combining Systems (FroCoS 2021). Birmingham, UK: Springer.
Export
BibTeX
@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ö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
Ebner, G., Blanchette, J. C., & Tourret, S. (2021). A Unifying Splitting Framework. In Automated Deduction - CADE 28. Virtual Event: Springer. doi:10.1007/978-3-030-79876-5_20
Export
BibTeX
@inproceedings{Ebner_CADE21,
TITLE = {A Unifying Splitting Framework},
AUTHOR = {Ebner, Gabriel and Blanchette, Jasmin Christian 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 Christian
%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é; Sutcliffe, Geof
%P 344 - 360
%I Springer
%@ 978-3-030-79875-8
%B Lecture Notes in Artificial Intelligence
%N 12699
England, M., Koepf, W., Sadykov, T., Seiler, W. M., & Sturm, T. (2021). Foreword, with a Dedication to Andreas Weber. Mathematics in Computer Science, 15. doi:10.1007/s11786-020-00476-y
Export
BibTeX
@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
England, M., Boulier, F., Sadykov, T., & Sturm, T. (2021). Foreword, with a Dedication to Vladimir Gerdt. Mathematics in Computer Science, 15. doi:10.1007/s11786-021-00509-0
Export
BibTeX
@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ç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
Frohn, F., Hark, M., & Giesl, J. (2021). Termination of Polynomial Loops. In Static Analysis (SAS 2020). Chicago, IL, USA (Online Event): Springer. doi:10.1007/978-3-030-65474-0_5
Export
BibTeX
@inproceedings{Frohn_SAS2020,
TITLE = {Termination of Polynomial Loops},
AUTHOR = {Frohn, Florian and Hark, M. 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, M.
%A Giesl, Jü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
Grigoriev, D., Iosif, A., Rahkooy, H., Sturm, T., & Weber, A. (2021). Efficiently and Effectively Recognizing Toricity of Steady State Varieties. Mathematics in Computer Science, 15. doi:10.1007/s11786-020-00479-9
Export
BibTeX
@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
Haifani, F., Tourret, S., & Weidenbach, C. (2021). Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance. In Automated Deduction - CADE 28. Virtual Event: Springer. doi:10.1007/978-3-030-79876-5_19
Export
BibTeX
@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é; Sutcliffe, Geof
%P 327 - 343
%I Springer
%@ 978-3-030-79875-8
%B Lecture Notes in Artificial Intelligence
%N 12699
Nummelin, V., Bentkamp, A., Tourret, S., & Vukmirović, P. (2021). Superposition with First-class Booleans and Inprocessing Clausification. In Automated Deduction - CADE 28. Virtual Event: Springer. doi:10.1007/978-3-030-79876-5_22
Export
BibTeX
@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ć, 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é; Sutcliffe, Geof
%P 378 - 395
%I Springer
%@ 978-3-030-79875-8
%B Lecture Notes in Artificial Intelligence
%N 12699
Rahkooy, H., & Vargas Montero, C. (2021). 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: IEEE. doi:10.1109/SYNASC51798.2020.00027
Export
BibTeX
@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
Rahkooy, H., & Sturm, T. (2021a). Parametric Toricity of Steady State Varieties of Reaction Networks. Retrieved from https://arxiv.org/abs/2105.10853
(arXiv: 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.
Export
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 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.},
}
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
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.
%K Quantitative Biology, Molecular Networks, q-bio.MN,Computer Science, Logic in Computer Science, cs.LO,Computer Science, Symbolic Computation, cs.SC,
Rahkooy, H., & Sturm, T. (2021b). Parametric Toricity of Steady State Varieties of Reaction Networks. In Computer Algebra in Scientific Computing (CASC 2021). Sochi, Russia: Springer. doi:10.1007/978-3-030-85165-1_18
Export
BibTeX
@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 Scientific Computing
%Z date of event: 2021-09-13 - 2021-09-17
%C Sochi, Russia
%B Computer Algebra in Scientific Computing
%E Boulier, Franç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
Rahkooy, H., & Sturm, T. (2021c). Testing Binomiality of Chemical Reaction Networks Using Comprehensive Gröbner Systems. In Computer Algebra in Scientific Computing (CASC 2021). Sochi, Russia: Springer. doi:10.1007/978-3-030-85165-1_19
Export
BibTeX
@inproceedings{Rahkooy_CASC2021b,
TITLE = {Testing Binomiality of Chemical Reaction Networks Using Comprehensive {Grö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ö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 Scientific Computing
%Z date of event: 2021-09-13 - 2021-09-17
%C Sochi, Russia
%B Computer Algebra in Scientific Computing
%E Boulier, Franç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
Rahkooy, H., & Sturm, T. (2021d). Testing Binomiality of Chemical Reaction Networks Using Comprehensive Gröbner Systems. Retrieved from https://arxiv.org/abs/2107.01706
(arXiv: 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.
Export
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 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.},
}
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ö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
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.
%K Quantitative Biology, Molecular Networks, q-bio.MN,Computer Science, Symbolic Computation, cs.SC
Schurr, H.-J., Fleury, M., & Desharnais, M. (2021). Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant. In Automated Deduction - CADE 28. Virtual Event: Springer. doi:10.1007/978-3-030-79876-5_26
Export
BibTeX
@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ö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é; Sutcliffe, Geof
%P 450 - 467
%I Springer
%@ 978-3-030-79875-8
%B Lecture Notes in Artificial Intelligence
%N 12699
Seiler, W. M., Seiß, M., & Sturm, T. (2021). A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations. Mathematics in Computer Science, 15. doi:10.1007/s11786-020-00485-x
Export
BibTeX
@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ß, 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
Tourret, S., & Blanchette, J. C. (2021). A Modular Isabelle Framework for Verifying Saturation Provers. In CPP ’21, 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. Virtual, Denmark: ACM. doi:10.1145/3437992.3439912
Export
BibTeX
@inproceedings{Tourret_CPP2021,
TITLE = {A modular {I}sabelle framework for verifying saturation provers},
AUTHOR = {Tourret, Sophie and Blanchette, Jasmin Christian},
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 Christian
%+ 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ţcu, Cătălin; Popescu, Andrei
%P 224 - 237
%I ACM
%@ 978-1-4503-8299-1
Vukmirović, P., Blanchette, J. C., Cruanes, S., & Schulz, S. (2021). Extending a Brainiac Prover to Lambda-Free Higher-Order Logic. International Journal on Software Tools for Technology Transfer (STTT). doi:10.1007/s10009-021-00639-7
Export
BibTeX
@article{Vukmirovic2021,
TITLE = {Extending a Brainiac Prover to Lambda-Free Higher-Order Logic},
AUTHOR = {Vukmirovi{\'c}, Petar and Blanchette, Jasmin Christian and Cruanes, Simon and Schulz, Stephan},
LANGUAGE = {eng},
ISSN = {1433-2779},
DOI = {10.1007/s10009-021-00639-7},
PUBLISHER = {Springer},
ADDRESS = {Berlin},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
JOURNAL = {International Journal on Software Tools for Technology Transfer (STTT)},
}
Endnote
%0 Journal Article
%A Vukmirović, Petar
%A Blanchette, Jasmin Christian
%A Cruanes, Simon
%A Schulz, Stephan
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
%T Extending a Brainiac Prover to Lambda-Free Higher-Order Logic :
%G eng
%U http://hdl.handle.net/21.11116/0000-0009-2A64-8
%R 10.1007/s10009-021-00639-7
%7 2021
%D 2021
%J International Journal on Software Tools for Technology Transfer (STTT)
%I Springer
%C Berlin
%@ false
Vukmirović, P., Bentkamp, A., Blanchette, J. C., Cruanes, S., Nummelin, V., & Tourret, S. (2021). Making Higher-Order Superposition Work. In Automated Deduction - CADE 28. Virtual Event: Springer. doi:10.1007/978-3-030-79876-5_24
Export
BibTeX
@inproceedings{Vukmirovic_CADE21,
TITLE = {Making Higher-Order Superposition Work},
AUTHOR = {Vukmirovi{\'c}, Petar and Bentkamp, Alexander and Blanchette, Jasmin Christian 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ć, Petar
%A Bentkamp, Alexander
%A Blanchette, Jasmin Christian
%A Cruanes, Simon
%A Nummelin, Visa
%A Tourret, Sophie
%+ External Organizations
External Organizations
External Organizations
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é; Sutcliffe, Geof
%P 415 - 432
%I Springer
%@ 978-3-030-79875-8
%B Lecture Notes in Artificial Intelligence
%N 12699