The Year Before Last

Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P., & Waldmann, U. (2021a). Superposition with Lambdas. Journal of Automated Reasoning, 65. doi:10.1007/s10817-021-09595-y

Links

[DOI]

[PuRe]

[BibTeX]

[publisher version]

Export

BibTeX

@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ć, 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., Tourret, S., & Vukmirović, P. (2021). Superposition for Full Higher-order Logic. In Automated Deduction - CADE 28. Virtual Event: Springer. doi:10.1007/978-3-030-79876-5_23

Links

Export

BibTeX

@inproceedings{Bentkamp_CADE21, TITLE = {Superposition for Full Higher-order Logic}, AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin and Tourret, Sophie and Vukmirovi{\'c}, Petar}, 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 %A Tourret, Sophie %A Vukmirović, 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 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., Tourret, S., Vukmirović, P., & Waldmann, U. (2021b). 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.

Links

Export

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 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 %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., Cruanes, S., & Waldmann, U. (2021). Superposition for Lambda-Free Higher-Order Logic. Logical Methods in Computer Science, 17(2). doi:10.23638/LMCS-17(2:1)2021

Links

Export

BibTeX

@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

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

Links

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. In Frontiers of Combining Systems (FroCoS 2021). Birmingham, UK: Springer.

Links

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

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

Links

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

Ebner, G., Blanchette, J., & Tourret, S. (2021). A Unifying Splitting Framework. In Automated Deduction - CADE 28. Virtual Event: Springer. doi:10.1007/978-3-030-79876-5_20

Links

Export

BibTeX

@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é; 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

Links

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

Links

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

Links

Export

BibTeX

@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ü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. (2021a). Efficiently and Effectively Recognizing Toricity of Steady State Varieties. Mathematics in Computer Science, 15. doi:10.1007/s11786-020-00479-9

Links

Export

BibTeX

@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

Grigoriev, D., Iosif, A., Rahkooy, H., Sturm, T., & Weber, A. (2021b). Efficiently and Effectively Recognizing Toricity of Steady State Varieties. Mathematics in Computer Science, 15. doi:10.1007/s11786-020-00479-9

Links

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

Links

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

Haifani, F., Koopmann, P., & Tourret, S. (2021). Abduction in EL via Translation to FOL. In Second-Order Quantifier Elimination and Related Topics (SOQE 2021). Online Event: CEUR-WS. Retrieved from urn:nbn:de:0074-3009-1

Links

Export

BibTeX

@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

Kruff, N., Lüders, C., Radulescu, O., Sturm, T., & Walcher, S. (2021). Algorithmic Reduction of Biological Networks With Multiple Time Scales. Mathematics in Computer Science, 15. doi:10.1007/s11786-021-00515-2

Links

Export

BibTeX

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

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

Links

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

Links

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. In Computer Algebra in Scientific Computing (CASC 2021). Sochi, Russia: Springer. doi:10.1007/978-3-030-85165-1_18

Links

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 Scientiﬁc 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. (2021b). 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.

Links

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. (2021c). 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.

Links

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

Rahkooy, H., & Sturm, T. (2021d). 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

Links

Export

BibTeX

@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ö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ﬁc 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

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

Links

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

Links

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

Sutcliffe, G., & Desharnais, M. (2021). The CADE-28 Automated Theorem Proving System Competition - CASC-28. AI Communications, 34(4). doi:10.3233/AIC-210235

Links

Export

BibTeX

@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

Tourret, S., & Blanchette, J. (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

Links

Export

BibTeX

@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ţcu, Cătălin; Popescu, Andrei %P 224 - 237 %I ACM %@ 978-1-4503-8299-1

Voigt, M. (2021). Decidable ∃∗∀∗ First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates. Journal of Automated Reasoning, 65. doi:10.1007/s10817-020-09567-8

Links

Export

BibTeX

@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 ∃∗∀∗ 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

Vukmirović, P., Bentkamp, A., Blanchette, J., 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

Links

Export

BibTeX

@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ć, 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é; Sutcliffe, Geof %P 415 - 432 %I Springer %@ 978-3-030-79875-8 %B Lecture Notes in Artificial Intelligence %N 12699