# Last Year

Barbosa, H., Blanchette, J. C., & Fontaine, P. (2020). Scalable Fine-Grained Proofs for Formula Processing.

*Journal of Automated Reasoning*,*64*(3). doi:10.1007/s10817-018-09502-yExport

BibTeX

@article{Barbosa2020,
TITLE = {Scalable Fine-Grained Proofs for Formula Processing},
AUTHOR = {Barbosa, Haniel and Blanchette, Jasmin Christian and Fontaine, Pascal},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-018-09502-y},
PUBLISHER = {D. Reidel Pub. Co.},
ADDRESS = {Dordrecht, Holland},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2020},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {64},
NUMBER = {3},
PAGES = {485--510},
}

Endnote

%0 Journal Article
%A Barbosa, Haniel
%A Blanchette, Jasmin Christian
%A Fontaine, Pascal
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Scalable Fine-Grained Proofs for Formula Processing :
%G eng
%U http://hdl.handle.net/21.11116/0000-0006-908A-B
%R 10.1007/s10817-018-09502-y
%7 2020
%D 2020
%J Journal of Automated Reasoning
%V 64
%N 3
%& 485
%P 485 - 510
%I D. Reidel Pub. Co.
%C Dordrecht, Holland
%@ false

Biere, A., Tinelli, C., & Weidenbach, C. (2020). Preface to the Special Issue on Automated Reasoning Systems.

*Journal of Automated Reasoning*,*64*(3). doi:10.1007/s10817-019-09531-1Export

BibTeX

@article{Biere2020,
TITLE = {Preface to the Special Issue on Automated Reasoning Systems},
AUTHOR = {Biere, Armin and Tinelli, Cesare and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-019-09531-1},
PUBLISHER = {D. Reidel Pub. Co.},
ADDRESS = {Dordrecht, Holland},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2020},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {64},
NUMBER = {3},
PAGES = {361--362},
}

Endnote

%0 Journal Article
%A Biere, Armin
%A Tinelli, Cesare
%A Weidenbach, Christoph
%+ External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Preface to the Special Issue on Automated Reasoning Systems :
%G eng
%U http://hdl.handle.net/21.11116/0000-0006-908E-7
%R 10.1007/s10817-019-09531-1
%7 2020
%D 2020
%J Journal of Automated Reasoning
%V 64
%N 3
%& 361
%P 361 - 362
%I D. Reidel Pub. Co.
%C Dordrecht, Holland
%@ false

Bradford, R., Davenport, J. H., England, M., Errami, H., Gerdt, V., Grigoriev, D., … Weber, A. (2020). Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks.

*Journal of Symbolic Computation*,*98*. doi:10.1016/j.jsc.2019.07.008Export

BibTeX

@article{BradfordDavenport:19a,
TITLE = {Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks},
AUTHOR = {Bradford, Russell and Davenport, James H. and England, Matthew and Errami, Hassan and Gerdt, Vladimir and Grigoriev, Dima and Hoyt, Charles and Ko{\v s}ta, Marek and Radulescu, Ovidiu and Sturm, Thomas and Weber, Andreas},
LANGUAGE = {eng},
ISSN = {0747-7171},
DOI = {10.1016/j.jsc.2019.07.008},
PUBLISHER = {Academic Press},
ADDRESS = {London},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2020},
JOURNAL = {Journal of Symbolic Computation},
VOLUME = {98},
PAGES = {84--119},
}

Endnote

%0 Journal Article
%A Bradford, Russell
%A Davenport, James H.
%A England, Matthew
%A Errami, Hassan
%A Gerdt, Vladimir
%A Grigoriev, Dima
%A Hoyt, Charles
%A Košta, Marek
%A Radulescu, Ovidiu
%A Sturm, Thomas
%A Weber, Andreas
%+ External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks :
%G eng
%U http://hdl.handle.net/21.11116/0000-0002-F04B-B
%R 10.1016/j.jsc.2019.07.008
%7 2020
%D 2020
%J Journal of Symbolic Computation
%V 98
%& 84
%P 84 - 119
%I Academic Press
%C London
%@ false

Bromberger, M., Sturm, T., & Weidenbach, C. (2020). A Complete and Terminating Approach to Linear Integer Solving.

*Journal of Symbolic Computation*,*100*. doi:10.1016/j.jsc.2019.07.021Export

BibTeX

@article{Bromberger2020,
TITLE = {A Complete and Terminating Approach to Linear Integer Solving},
AUTHOR = {Bromberger, Martin and Sturm, Thomas and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {0747-7171},
DOI = {10.1016/j.jsc.2019.07.021},
PUBLISHER = {Academic Press},
ADDRESS = {London},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2020},
JOURNAL = {Journal of Symbolic Computation},
VOLUME = {100},
PAGES = {102--136},
}

Endnote

%0 Journal Article
%A Bromberger, Martin
%A Sturm, Thomas
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T A Complete and Terminating Approach to Linear Integer Solving :
%G eng
%U http://hdl.handle.net/21.11116/0000-0006-99CD-7
%R 10.1016/j.jsc.2019.07.021
%7 2019
%D 2020
%J Journal of Symbolic Computation
%V 100
%& 102
%P 102 - 136
%I Academic Press
%C London
%@ false

Bromberger, M., Fiori, A., & Weidenbach, C. (2020). SCL with Theory Constraints. Retrieved from https://arxiv.org/abs/2003.04627

(arXiv: 2003.04627) Abstract

We lift the SCL calculus for first-order logic without equality to the SCL(T)
calculus for first-order logic without equality modulo a background theory. In
a nutshell, the SCL(T) calculus describes a new way to guide hierarchic
resolution inferences by a partial model assumption instead of an a priori
fixed order as done for instance in hierarchic superposition. The model
representation consists of ground background theory literals and ground
foreground first-order literals. One major advantage of the model guided
approach is that clauses generated by SCL(T) enjoy a non-redundancy property
that makes expensive testing for tautologies and forward subsumption completely
obsolete. SCL(T) is a semi-decision procedure for pure clause sets that are
clause sets without first-order function symbols ranging into the background
theory sorts. Moreover, SCL(T) can be turned into a decision procedure if the
considered combination of a first-order logic modulo a background theory enjoys
an abstract finite model property.

Export

BibTeX

@online{DBLP:journals/corr/abs-2003-04627,
TITLE = {{SCL} with Theory Constraints},
AUTHOR = {Bromberger, Martin and Fiori, Alberto and Weidenbach, Christoph},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/2003.04627},
EPRINT = {2003.04627},
EPRINTTYPE = {arXiv},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
ABSTRACT = {We lift the SCL calculus for first-order logic without equality to the SCL(T) calculus for first-order logic without equality modulo a background theory. In a nutshell, the SCL(T) calculus describes a new way to guide hierarchic resolution inferences by a partial model assumption instead of an a priori fixed order as done for instance in hierarchic superposition. The model representation consists of ground background theory literals and ground foreground first-order literals. One major advantage of the model guided approach is that clauses generated by SCL(T) enjoy a non-redundancy property that makes expensive testing for tautologies and forward subsumption completely obsolete. SCL(T) is a semi-decision procedure for pure clause sets that are clause sets without first-order function symbols ranging into the background theory sorts. Moreover, SCL(T) can be turned into a decision procedure if the considered combination of a first-order logic modulo a background theory enjoys an abstract finite model property.},
}

Endnote

%0 Report
%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 SCL with Theory Constraints :
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-7AFE-3
%U https://arxiv.org/abs/2003.04627
%D 2020
%X We lift the SCL calculus for first-order logic without equality to the SCL(T)
calculus for first-order logic without equality modulo a background theory. In
a nutshell, the SCL(T) calculus describes a new way to guide hierarchic
resolution inferences by a partial model assumption instead of an a priori
fixed order as done for instance in hierarchic superposition. The model
representation consists of ground background theory literals and ground
foreground first-order literals. One major advantage of the model guided
approach is that clauses generated by SCL(T) enjoy a non-redundancy property
that makes expensive testing for tautologies and forward subsumption completely
obsolete. SCL(T) is a semi-decision procedure for pure clause sets that are
clause sets without first-order function symbols ranging into the background
theory sorts. Moreover, SCL(T) can be turned into a decision procedure if the
considered combination of a first-order logic modulo a background theory enjoys
an abstract finite model property.
%K Computer Science, Logic in Computer Science, cs.LO

Davenport, J. H., England, M., Griggio, A., Sturm, T., & Tinelli, C. (2020). Symbolic Computation and Satisfiability Checking.

*Journal of Symbolic Computation*,*100*. doi:10.1016/j.jsc.2019.07.017Export

BibTeX

@article{Davenport2020,
TITLE = {Symbolic Computation and Satisfiability Checking},
AUTHOR = {Davenport, James H. and England, Matthew and Griggio, Alberto and Sturm, Thomas and Tinelli, Cesare},
LANGUAGE = {eng},
ISSN = {0747-7171},
DOI = {10.1016/j.jsc.2019.07.017},
PUBLISHER = {Academic Press},
ADDRESS = {London},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2020},
JOURNAL = {Journal of Symbolic Computation},
VOLUME = {100},
PAGES = {1--10},
}

Endnote

%0 Journal Article
%A Davenport, James H.
%A England, Matthew
%A Griggio, Alberto
%A Sturm, Thomas
%A Tinelli, Cesare
%+ External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Symbolic Computation and Satisfiability Checking : Editorial
%G eng
%U http://hdl.handle.net/21.11116/0000-0006-99CF-5
%R 10.1016/j.jsc.2019.07.017
%7 2020
%D 2020
%J Journal of Symbolic Computation
%V 100
%& 1
%P 1 - 10
%I Academic Press
%C London
%@ false

England, M., Koepf, W., Sadykov, T., Seiler, W. M., & Sturm, T. (2020). Foreword, with a Dedication to Andreas Weber.

*Mathematics in Computer Science*. doi:10.1007/s11786-020-00476-yExport

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 = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2020},
JOURNAL = {Mathematics in Computer Science},
}

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 2020
%J Mathematics in Computer Science
%I Springer
%C New York, NY
%@ false
%U https://rdcu.be/cbpdy

Faqeh, R., Fetzer, C., Hermanns, H., Hoffmann, J., Klauck, M., Köhl, M. A., … Weidenbach, C. (2020). Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification. In

*Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles*. Rhodes, Greece (Virtual Event): Springer. doi:10.1007/978-3-030-61470-6_25Export

BibTeX

@inproceedings{DBLP:conf/isola/FaqehFH0KKSW20,
TITLE = {Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification},
AUTHOR = {Faqeh, Rasha and Fetzer, Christof and Hermanns, Holger and Hoffmann, J{\"o}rg and Klauck, Michaela and K{\"o}hl, Maximilian A. and Steinmetz, Marcel and Weidenbach, Christoph},
LANGUAGE = {eng},
ISBN = {978-3-030-61469-0},
DOI = {10.1007/978-3-030-61470-6_25},
PUBLISHER = {Springer},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2020},
BOOKTITLE = {Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles},
EDITOR = {Margaria, Tiziana and Steffen, Bernhard},
PAGES = {416--439},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {12477},
ADDRESS = {Rhodes, Greece (Virtual Event)},
}

Endnote

%0 Conference Proceedings
%A Faqeh, Rasha
%A Fetzer, Christof
%A Hermanns, Holger
%A Hoffmann, Jörg
%A Klauck, Michaela
%A Köhl, Maximilian A.
%A Steinmetz, Marcel
%A Weidenbach, Christoph
%+ External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification :
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-7B0E-1
%R 10.1007/978-3-030-61470-6_25
%D 2020
%B 9th International Symposium on Leveraging Applications of Formal Methods, Veriﬁcation and Validation
%Z date of event: 2020-10-20 - 2020-10-30
%C Rhodes, Greece (Virtual Event)
%B Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles
%E Margaria, Tiziana; Steffen, Bernhard
%P 416 - 439
%I Springer
%@ 978-3-030-61469-0
%B Lecture Notes in Computer Science
%N 12477

Fleury, M. (2020).

*Formalization of Logical Calculi in Isabelle/HOL*. Universität des Saarlandes, Saarbrücken.Abstract

I develop a formal framework for propositional satifisfiability with the conflict-driven clause learning (CDCL) procedure using the Isabelle/HOL proof assistant. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis-Putnam-Logemann-Loveland procedure. The most noteworthy aspects of my work are the inclusion of rules for forget and restart and the refinement approach. I use the formalization to develop three extensions: First, an incremental solving extension of CDCL. Second, I verify an optimizing CDCL (OCDCL): Given a cost function on literals, OCDCL derives an optimal model with minimum cost. Finally, I work on model covering. Thanks to the CDCL framework I can reuse, these extensions are easier to develop. Through a chain of refinements, I connect the abstract CDCL calculus first to a more concrete calculus, then to a SAT solver expressed in a simple functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The imperative version relies on the two-watched-literal data structure and other optimizations found in modern solvers. I used the Isabelle Refinement Framework to automate the most tedious refinement steps. After that, I extend this work with further optimizations like blocking literals and the use of machine words as long as possible, before switching to unbounded integers to keep completeness.

Export

BibTeX

@phdthesis{Fleuryphd2019,
TITLE = {Formalization of Logical Calculi in Isabelle/{HOL}},
AUTHOR = {Fleury, Mathias},
LANGUAGE = {eng},
DOI = {10.22028/D291-30179},
SCHOOL = {Universit{\"a}t des Saarlandes},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2020},
ABSTRACT = {I develop a formal framework for propositional satifisfiability with the conflict-driven clause learning (CDCL) procedure using the Isabelle/HOL proof assistant. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis-Putnam-Logemann-Loveland procedure. The most noteworthy aspects of my work are the inclusion of rules for forget and restart and the refinement approach. I use the formalization to develop three extensions: First, an incremental solving extension of CDCL. Second, I verify an optimizing CDCL (OCDCL): Given a cost function on literals, OCDCL derives an optimal model with minimum cost. Finally, I work on model covering. Thanks to the CDCL framework I can reuse, these extensions are easier to develop. Through a chain of refinements, I connect the abstract CDCL calculus first to a more concrete calculus, then to a SAT solver expressed in a simple functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The imperative version relies on the two-watched-literal data structure and other optimizations found in modern solvers. I used the Isabelle Refinement Framework to automate the most tedious refinement steps. After that, I extend this work with further optimizations like blocking literals and the use of machine words as long as possible, before switching to unbounded integers to keep completeness.},
}

Endnote

%0 Thesis
%A Fleury, Mathias
%Y Weidenbach, Christoph
%A referee: Biere, Armin
%+ Automation of Logic, MPI for Informatics, Max Planck Society
International Max Planck Research School, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Formalization of Logical Calculi in Isabelle/HOL :
%G eng
%U http://hdl.handle.net/21.11116/0000-0005-AE07-0
%R 10.22028/D291-30179
%I Universität des Saarlandes
%C Saarbrücken
%D 2020
%P 169 p.
%V phd
%9 phd
%X I develop a formal framework for propositional satifisfiability with the conflict-driven clause learning (CDCL) procedure using the Isabelle/HOL proof assistant. The framework offers a convenient way to prove metatheorems and experiment with variants, including the Davis-Putnam-Logemann-Loveland procedure. The most noteworthy aspects of my work are the inclusion of rules for forget and restart and the refinement approach. I use the formalization to develop three extensions: First, an incremental solving extension of CDCL. Second, I verify an optimizing CDCL (OCDCL): Given a cost function on literals, OCDCL derives an optimal model with minimum cost. Finally, I work on model covering. Thanks to the CDCL framework I can reuse, these extensions are easier to develop. Through a chain of refinements, I connect the abstract CDCL calculus first to a more concrete calculus, then to a SAT solver expressed in a simple functional programming language, and finally to a SAT solver in an imperative language, with total correctness guarantees. The imperative version relies on the two-watched-literal data structure and other optimizations found in modern solvers. I used the Isabelle Refinement Framework to automate the most tedious refinement steps. After that, I extend this work with further optimizations like blocking literals and the use of machine words as long as possible, before switching to unbounded integers to keep completeness.
%U https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/28722

Fleury, M., & Weidenbach, C. (2020). A Verified SAT Solver Framework including Optimization and Partial Valuations. In

*LPAR-23, 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning*. Virtual Conferernce: EasyChair. doi:10.29007/96wbExport

BibTeX

@inproceedings{DBLP:conf/lpar/FleuryW20,
TITLE = {A Verified {SAT} Solver Framework including Optimization and Partial Valuations},
AUTHOR = {Fleury, Mathias and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {2040-557X},
DOI = {10.29007/96wb},
PUBLISHER = {EasyChair},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
BOOKTITLE = {LPAR-23, 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
EDITOR = {Albert, Elvira and Kov{\'a}cs, Laura},
PAGES = {212--229},
SERIES = {EasyChair Proceedings in Computing},
VOLUME = {73},
ADDRESS = {Virtual Conferernce},
}

Endnote

%0 Conference Proceedings
%A Fleury, Mathias
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T A Verified SAT Solver Framework including Optimization and Partial Valuations :
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-78C7-2
%R 10.29007/96wb
%D 2020
%B 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
%Z date of event: 2021-01-12 - 2021-01-13
%C Virtual Conferernce
%B LPAR-23
%E Albert, Elvira; Kovács, Laura
%P 212 - 229
%I EasyChair
%B EasyChair Proceedings in Computing
%N 73
%@ false
%U https://easychair.org/publications/paper/b7Cr

Frohn, F. (2020). A Calculus for Modular Loop Acceleration. In

*Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020)*. Dublin, Ireland (Online Event): Springer. doi:10.1007/978-3-030-45190-5_4Export

BibTeX

@inproceedings{Frohn_TACAS2020,
TITLE = {A Calculus for Modular Loop Acceleration},
AUTHOR = {Frohn, Florian},
LANGUAGE = {eng},
ISBN = {978-3-030-45189-9},
DOI = {10.1007/978-3-030-45190-5_4},
PUBLISHER = {Springer},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2020},
BOOKTITLE = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020)},
EDITOR = {Biere, Armin and Parker, David},
PAGES = {58--76},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {12078},
ADDRESS = {Dublin, Ireland (Online Event)},
}

Endnote

%0 Conference Proceedings
%A Frohn, Florian
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T A Calculus for Modular Loop Acceleration :
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-7FCF-3
%R 10.1007/978-3-030-45190-5_4
%D 2020
%B 26th International Conference on Tools and Algorithms for the Construction and Analysis of System
%Z date of event: 2020-04-25 - 2020-04-30
%C Dublin, Ireland (Online Event)
%B Tools and Algorithms for the Construction and Analysis of Systems
%E Biere, Armin; Parker, David
%P 58 - 76
%I Springer
%@ 978-3-030-45189-9
%B Lecture Notes in Computer Science
%N 12078

Frohn, F., Naaf, M., Brockschmidt, M., & Giesl, J. (2020). Inferring Lower Runtime Bounds for Integer Programs.

*ACM Transactions on Programming Languages and Systems*,*42*. doi:10.1145/3410331Export

BibTeX

@article{Frohn_TPLS2020,
TITLE = {Inferring Lower Runtime Bounds for Integer Programs},
AUTHOR = {Frohn, Florian and Naaf, Matthias and Brockschmidt, Marc and Giesl, J{\"u}rgen},
LANGUAGE = {eng},
ISSN = {0164-0925},
DOI = {10.1145/3410331},
PUBLISHER = {ACM},
ADDRESS = {New York, NY},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
JOURNAL = {ACM Transactions on Programming Languages and Systems},
VOLUME = {42},
EID = {13},
}

Endnote

%0 Journal Article
%A Frohn, Florian
%A Naaf, Matthias
%A Brockschmidt, Marc
%A Giesl, Jürgen
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
External Organizations
%T Inferring Lower Runtime Bounds for Integer Programs :
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-7FCD-5
%R 10.1145/3410331
%7 2020
%D 2020
%J ACM Transactions on Programming Languages and Systems
%V 42
%Z sequence number: 13
%I ACM
%C New York, NY
%@ false

Frohn, F., Hark, M., & Giesl, J. (n.d.). Termination for Polynomial Loops. In

(Accepted/in press) *Static Analysis (SAS 2020)*. Chicago, IL, USA (Online Event): Springer.Export

BibTeX

@inproceedings{Frohn_SAS2020,
TITLE = {Termination for Polynomial Loops},
AUTHOR = {Frohn, Florian and Hark, M. and Giesl, J{\"u}rgen},
LANGUAGE = {eng},
PUBLISHER = {Springer},
YEAR = {2020},
PUBLREMARK = {Accepted},
MARGINALMARK = {$\bullet$},
BOOKTITLE = {Static Analysis (SAS 2020)},
SERIES = {Lecture Notes in Computer Science},
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 for Polynomial Loops :
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-7FE3-B
%D 2020
%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
%I Springer
%B Lecture Notes in Computer Science

Grigoriev, D., Iosif, A., Rahkooy, H., Sturm, T., & Weber, A. (2020). Efficiently and Effectively Recognizing Toricity of Steady State Varieties.

*Mathematics in Computer Science*. doi:10.1007/s11786-020-00479-9Export

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 = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2020},
JOURNAL = {Mathematics in Computer Science},
}

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 2020
%J Mathematics in Computer Science
%I Springer
%C New York, NY
%@ false
%U https://rdcu.be/cbpcc

Haifani, F., Koopmann, P., Tourret, S., & Weidenbach, C. (2020). On a Notion of Relevance. In

*Proceedings of the 33rd International Workshop on Description Logics (DL 2020)*. Rhodes, Greece (Virtual Event): ceur-ws.org. Retrieved from http://ceur-ws.org/Vol-2663/paper-10.pdf; urn:nbn:de:0074-2663-4Export

BibTeX

@inproceedings{Haifani_DL2020,
TITLE = {On a Notion of Relevance},
AUTHOR = {Haifani, Fajar and Koopmann, Patrick and Tourret, Sophie and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {1613-0073},
URL = {http://ceur-ws.org/Vol-2663/paper-10.pdf; urn:nbn:de:0074-2663-4},
PUBLISHER = {ceur-ws.org},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
BOOKTITLE = {Proceedings of the 33rd International Workshop on Description Logics (DL 2020)},
EDITOR = {Borgwardt, Stefan and Meyer, Thomas},
EID = {10},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {2663},
ADDRESS = {Rhodes, Greece (Virtual Event)},
}

Endnote

%0 Conference Proceedings
%A Haifani, Fajar
%A Koopmann, Patrick
%A Tourret, Sophie
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T On a Notion of Relevance :
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-7968-D
%U http://ceur-ws.org/Vol-2663/paper-10.pdf
%D 2020
%B 33rd International Workshop on Description Logics
%Z date of event: 2020-09-12 - 2020-09-14
%C Rhodes, Greece (Virtual Event)
%B Proceedings of the 33rd International Workshop on Description Logics
%E Borgwardt , Stefan; Meyer, Thomas
%Z sequence number: 10
%I ceur-ws.org
%B CEUR Workshop Proceedings
%N 2663
%@ false

Hark, M., Frohn, F., & Giesl, J. (2020). Polynomial Loops: Beyond Termination. In

*LPAR-23, 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning*. Virtual Conferernce: EasyChair. doi:10.29007/nxv1Export

BibTeX

@inproceedings{Hark_LPAR-23,
TITLE = {Polynomial Loops: Beyond Termination},
AUTHOR = {Hark, Marcel and Frohn, Florian and Giesl, J{\"u}rgen},
LANGUAGE = {eng},
ISSN = {2040-557X},
DOI = {10.29007/nxv1},
PUBLISHER = {EasyChair},
YEAR = {2021},
MARGINALMARK = {$\bullet$},
BOOKTITLE = {LPAR-23, 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
EDITOR = {Albert, Elvira and Kov{\'a}cs, Laura},
PAGES = {279--297},
SERIES = {EasyChair Proceedings in Computing},
VOLUME = {73},
ADDRESS = {Virtual Conferernce},
}

Endnote

%0 Conference Proceedings
%A Hark, Marcel
%A Frohn, Florian
%A Giesl, Jürgen
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Polynomial Loops: Beyond Termination :
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-7FD4-C
%R 10.29007/nxv1
%D 2020
%B 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
%Z date of event: 2021-01-12 - 2021-01-13
%C Virtual Conferernce
%B LPAR-23
%E Albert, Elvira; Kovács, Laura
%P 279 - 297
%I EasyChair
%B EasyChair Proceedings in Computing
%N 73
%@ false
%U https://easychair.org/publications/paper/Bl5n

Koopmann, P., Del-Pinto, W., Tourret, S., & Schmidt, R. A. (2020). Signature-Based Abduction for Expressive Description Logics. In

*Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020)*. Rhodes, Greece (Virtual Conference): IJCAI Organization. doi:10.24963/kr.2020/59Export

BibTeX

@inproceedings{Koopmann_KR2020,
TITLE = {Signature-Based Abduction for Expressive Description Logics},
AUTHOR = {Koopmann, Patrick and Del-Pinto, Warren and Tourret, Sophie and Schmidt, Renate A.},
LANGUAGE = {eng},
ISBN = {978-0-9992411-7-2},
DOI = {10.24963/kr.2020/59},
PUBLISHER = {IJCAI Organization},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
BOOKTITLE = {Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020)},
EDITOR = {Calvanese, Diego and Erdem, Esra and Thielscher, Michael},
PAGES = {592--602},
ADDRESS = {Rhodes, Greece (Virtual Conference)},
}

Endnote

%0 Conference Proceedings
%A Koopmann, Patrick
%A Del-Pinto, Warren
%A Tourret, Sophie
%A Schmidt, Renate A.
%+ External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Signature-Based Abduction for Expressive Description Logics :
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-7961-4
%R 10.24963/kr.2020/59
%D 2020
%B 17th International Conference on Principles of Knowledge Representation and Reasoning
%Z date of event: 2020-09-12 - 2020-09-18
%C Rhodes, Greece (Virtual Conference)
%B Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning
%E Calvanese, Diego; Erdem, Esra; Thielscher, Michael
%P 592 - 602
%I IJCAI Organization
%@ 978-0-9992411-7-2
%U https://doi.org/10.24963/kr.2020/59

Kruff, N., Lüders, C., Radulescu, O., Sturm, T., & Walcher, S. (2020). Algorithmic Reduction of Biological Networks With Multiple Time Scales. Retrieved from https://arxiv.org/abs/2010.10129

(arXiv: 2010.10129) Abstract

We present a symbolic algorithmic approach that allows to compute invariant
manifolds and corresponding reduced systems for differential equations modeling
biological networks which comprise chemical reaction networks for cellular
biochemistry, and compartmental models for pharmacology, epidemiology and
ecology. Multiple time scales of a given network are obtained by scaling, based
on tropical geometry. Our reduction is mathematically justified within a
singular perturbation setting using a recent result by Cardin and Teixeira. The
existence of invariant manifolds is subject to hyperbolicity conditions, which
we test algorithmically using Hurwitz criteria. We finally obtain a sequence of
nested invariant manifolds and respective reduced systems on those manifolds.
Our theoretical results are generally accompanied by rigorous algorithmic
descriptions suitable for direct implementation based on existing off-the-shelf
software systems, specifically symbolic computation libraries and
Satisfiability Modulo Theories solvers. We present computational examples taken
from the well-known BioModels database using our own prototypical
implementations.

Export

BibTeX

@online{Kruff_arXiv2010.10129,
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},
URL = {https://arxiv.org/abs/2010.10129},
EPRINT = {2010.10129},
EPRINTTYPE = {arXiv},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
ABSTRACT = {We present a symbolic algorithmic approach that allows to compute invariant manifolds and corresponding reduced systems for differential equations modeling biological networks which comprise chemical reaction networks for cellular biochemistry, and compartmental models for pharmacology, epidemiology and ecology. Multiple time scales of a given network are obtained by scaling, based on tropical geometry. Our reduction is mathematically justified within a singular perturbation setting using a recent result by Cardin and Teixeira. The existence of invariant manifolds is subject to hyperbolicity conditions, which we test algorithmically using Hurwitz criteria. We finally obtain a sequence of nested invariant manifolds and respective reduced systems on those manifolds. Our theoretical results are generally accompanied by rigorous algorithmic descriptions suitable for direct implementation based on existing off-the-shelf software systems, specifically symbolic computation libraries and Satisfiability Modulo Theories solvers. We present computational examples taken from the well-known BioModels database using our own prototypical implementations.},
}

Endnote

%0 Report
%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-0007-7A12-C
%U https://arxiv.org/abs/2010.10129
%D 2020
%X We present a symbolic algorithmic approach that allows to compute invariant
manifolds and corresponding reduced systems for differential equations modeling
biological networks which comprise chemical reaction networks for cellular
biochemistry, and compartmental models for pharmacology, epidemiology and
ecology. Multiple time scales of a given network are obtained by scaling, based
on tropical geometry. Our reduction is mathematically justified within a
singular perturbation setting using a recent result by Cardin and Teixeira. The
existence of invariant manifolds is subject to hyperbolicity conditions, which
we test algorithmically using Hurwitz criteria. We finally obtain a sequence of
nested invariant manifolds and respective reduced systems on those manifolds.
Our theoretical results are generally accompanied by rigorous algorithmic
descriptions suitable for direct implementation based on existing off-the-shelf
software systems, specifically symbolic computation libraries and
Satisfiability Modulo Theories solvers. We present computational examples taken
from the well-known BioModels database using our own prototypical
implementations.
%K Quantitative Biology, Molecular Networks, q-bio.MN,Computer Science, Logic in Computer Science, cs.LO,Computer Science, Symbolic Computation, cs.SC,Mathematics, Dynamical Systems, math.DS,

Rahkooy, H., Radulescu, O., & Sturm, T. (2020). A Linear Algebra Approach for Detecting Binomiality of Steady State Ideals of Reversible Chemical Reaction Networks. In

*Computer Algebra in Scientific Computing (CASC 2020)*. Linz, Austria (Virtual Event): Springer. doi:10.1007/978-3-030-60026-6_29Export

BibTeX

@inproceedings{Rahkooy_CASC2020b,
TITLE = {A Linear Algebra Approach for Detecting Binomiality of Steady State Ideals of Reversible Chemical Reaction Networks},
AUTHOR = {Rahkooy, Hamid and Radulescu, Ovidiu and Sturm, Thomas},
LANGUAGE = {eng},
DOI = {10.1007/978-3-030-60026-6_29},
PUBLISHER = {Springer},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2020},
BOOKTITLE = {Computer Algebra in Scientific Computing (CASC 2020)},
EDITOR = {Boulier, Fran{\c c}ois and England, Matthew and Sadykov, Timur M. and Vorozhtsov, Evgenii V.},
PAGES = {492--509},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {12291},
ADDRESS = {Linz, Austria (Virtual Event)},
}

Endnote

%0 Conference Proceedings
%A Rahkooy, Hamid
%A Radulescu, Ovidiu
%A Sturm, Thomas
%+ External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T A Linear Algebra Approach for Detecting Binomiality of Steady State Ideals of Reversible Chemical Reaction Networks :
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-7A1C-2
%R 10.1007/978-3-030-60026-6_29
%D 2020
%B 22nd International Workshop on Computer Algebra in Scientific Computing
%Z date of event: 2020-09-14 - 2020-09-18
%C Linz, Austria (Virtual Event)
%B Computer Algebra in Scientific Computing
%E Boulier, François; England, Matthew; Sadykov, Timur M.; Vorozhtsov, Evgenii V.
%P 492 - 509
%I Springer
%B Lecture Notes in Computer Science
%N 12291

Rahkooy, H., & Sturm, T. (2020). First-Order Tests for Toricity. In

*Computer Algebra in Scientific Computing (CASC 2020)*. Linz, Austria (Virtual Event): Springer. doi:10.1007/978-3-030-60026-6_30Export

BibTeX

@inproceedings{Rahkooy_CASC2020,
TITLE = {First-Order Tests for Toricity},
AUTHOR = {Rahkooy, Hamid and Sturm, Thomas},
LANGUAGE = {eng},
DOI = {10.1007/978-3-030-60026-6_30},
PUBLISHER = {Springer},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2020},
BOOKTITLE = {Computer Algebra in Scientific Computing (CASC 2020)},
EDITOR = {Boulier, Fran{\c c}ois and England, Matthew and Sadykov, Timur M. and Vorozhtsov, Evgenii V.},
PAGES = {510--527},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {12291},
ADDRESS = {Linz, Austria (Virtual Event)},
}

Endnote

%0 Conference Proceedings
%A Rahkooy, Hamid
%A Sturm, Thomas
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T First-Order Tests for Toricity :
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-7A18-6
%R 10.1007/978-3-030-60026-6_30
%D 2020
%B 22nd International Workshop on Computer Algebra in Scientific Computing
%Z date of event: 2020-09-14 - 2020-09-18
%C Linz, Austria (Virtual Event)
%B Computer Algebra in Scientific Computing
%E Boulier, François; England, Matthew; Sadykov, Timur M.; Vorozhtsov, Evgenii V.
%P 510 - 527
%I Springer
%B Lecture Notes in Computer Science
%N 12291

Rahkooy, H., & Vargas Montero, C. (2020). A Graph Theoretical Approach for Testing Binomiality of Reversible Chemical Reaction Networks. Retrieved from https://arxiv.org/abs/2010.12615

(arXiv: 2010.12615) Abstract

We study binomiality of the steady state ideals of chemical reaction
networks. Considering rate constants as indeterminates, the concept of
unconditional binomiality has been introduced and an algorithm based on linear
algebra has been proposed in a recent work for reversible chemical reaction
networks, which has a polynomial time complexity upper bound on the number of
species and reactions. In this article, using a modified version of
species--reaction graphs, we present an algorithm based on graph theory which
performs by adding and deleting edges and changing the labels of the edges in
order to test unconditional binomiality. We have implemented our graph
theoretical algorithm as well as the linear algebra one in Maple and made
experiments on biochemical models. Our experiments show that the performance of
the graph theoretical approach is similar to or better than the linear algebra
approach, while it is drastically faster than Groebner basis and quantifier
elimination methods.

Export

BibTeX

@online{Rahkooy_arxiv2010.12615,
TITLE = {A Graph Theoretical Approach for Testing Binomiality of Reversible Chemical Reaction Networks},
AUTHOR = {Rahkooy, Hamid and Vargas Montero, Cristian},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/2010.12615},
EPRINT = {2010.12615},
EPRINTTYPE = {arXiv},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
ABSTRACT = {We study binomiality of the steady state ideals of chemical reaction networks. Considering rate constants as indeterminates, the concept of unconditional binomiality has been introduced and an algorithm based on linear algebra has been proposed in a recent work for reversible chemical reaction networks, which has a polynomial time complexity upper bound on the number of species and reactions. In this article, using a modified version of species--reaction graphs, we present an algorithm based on graph theory which performs by adding and deleting edges and changing the labels of the edges in order to test unconditional binomiality. We have implemented our graph theoretical algorithm as well as the linear algebra one in Maple and made experiments on biochemical models. Our experiments show that the performance of the graph theoretical approach is similar to or better than the linear algebra approach, while it is drastically faster than Groebner basis and quantifier elimination methods.},
}

Endnote

%0 Report
%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-0007-B427-2
%U https://arxiv.org/abs/2010.12615
%D 2020
%X We study binomiality of the steady state ideals of chemical reaction
networks. Considering rate constants as indeterminates, the concept of
unconditional binomiality has been introduced and an algorithm based on linear
algebra has been proposed in a recent work for reversible chemical reaction
networks, which has a polynomial time complexity upper bound on the number of
species and reactions. In this article, using a modified version of
species--reaction graphs, we present an algorithm based on graph theory which
performs by adding and deleting edges and changing the labels of the edges in
order to test unconditional binomiality. We have implemented our graph
theoretical algorithm as well as the linear algebra one in Maple and made
experiments on biochemical models. Our experiments show that the performance of
the graph theoretical approach is similar to or better than the linear algebra
approach, while it is drastically faster than Groebner basis and quantifier
elimination methods.
%K Computer Science, Symbolic Computation, cs.SC,Mathematics, Commutative Algebra, math.AC

Schlichtkrull, A., Blanchette, J. C., Traytel, D., & Waldmann, U. (2020). Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover.

*Journal of Automated Reasoning*. doi:10.1007/s10817-020-09561-0Export

BibTeX

@article{Schlichtkrull_JAR2020,
TITLE = {Formalizing {B}achmair and {G}anzinger's Ordered Resolution Prover},
AUTHOR = {Schlichtkrull, Anders and Blanchette, Jasmin Christian and Traytel, Dmitriy and Waldmann, Uwe},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-020-09561-0},
PUBLISHER = {D. Reidel Pub. Co.},
ADDRESS = {Dordrecht, Holland},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
JOURNAL = {Journal of Automated Reasoning},
}

Endnote

%0 Journal Article
%A Schlichtkrull, Anders
%A Blanchette, Jasmin Christian
%A Traytel, Dmitriy
%A Waldmann, Uwe
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Formalizing Bachmair and Ganzinger's Ordered Resolution Prover :
%G eng
%U http://hdl.handle.net/21.11116/0000-0006-A2B5-6
%R 10.1007/s10817-020-09561-0
%7 2020
%D 2020
%J Journal of Automated Reasoning
%I D. Reidel Pub. Co.
%C Dordrecht, Holland
%@ false

Seiler, W. M., Seiß, M., & Sturm, T. (2020). A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations.

*Mathematics in Computer Science*. doi:10.1007/s11786-020-00485-xExport

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 = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2020},
JOURNAL = {Mathematics in Computer Science},
}

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 2020
%J Mathematics in Computer Science
%I Springer
%C New York, NY
%@ false
%U https://rdcu.be/cbpcP

Seiler, W. M., Seiss, M., & Sturm, T. (2020). A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations. Retrieved from https://arxiv.org/abs/2003.00740

(arXiv: 2003.00740) Abstract

We discuss the effective computation of geometric singularities of implicit
ordinary differential equations over the real numbers using methods from logic.
Via the Vessiot theory of differential equations, geometric singularities can
be characterised as points where the behaviour of a certain linear system of
equations changes. These points can be discovered using a specifically adapted
parametric generalisation of Gaussian elimination combined with heuristic
simplification techniques and real quantifier elimination methods. We
demonstrate the relevance and applicability of our approach with computational
experiments using a prototypical implementation in Reduce.

Export

BibTeX

@online{Seiler_arXiv2003.00740,
TITLE = {A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations},
AUTHOR = {Seiler, Werner M. and Seiss, Matthias and Sturm, Thomas},
LANGUAGE = {eng},
URL = {https://arxiv.org/abs/2003.00740},
EPRINT = {2003.00740},
EPRINTTYPE = {arXiv},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
ABSTRACT = {We discuss the effective computation of geometric singularities of implicit ordinary differential equations over the real numbers using methods from logic. Via the Vessiot theory of differential equations, geometric singularities can be characterised as points where the behaviour of a certain linear system of equations changes. These points can be discovered using a specifically adapted parametric generalisation of Gaussian elimination combined with heuristic simplification techniques and real quantifier elimination methods. We demonstrate the relevance and applicability of our approach with computational experiments using a prototypical implementation in Reduce.},
}

Endnote

%0 Report
%A Seiler, Werner M.
%A Seiss, 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-7A09-7
%U https://arxiv.org/abs/2003.00740
%D 2020
%X We discuss the effective computation of geometric singularities of implicit
ordinary differential equations over the real numbers using methods from logic.
Via the Vessiot theory of differential equations, geometric singularities can
be characterised as points where the behaviour of a certain linear system of
equations changes. These points can be discovered using a specifically adapted
parametric generalisation of Gaussian elimination combined with heuristic
simplification techniques and real quantifier elimination methods. We
demonstrate the relevance and applicability of our approach with computational
experiments using a prototypical implementation in Reduce.
%K Mathematics, Logic, math.LO,Mathematics, Commutative Algebra, math.AC,Mathematics, Differential Geometry, math.DG,

Teucke, A., & Weidenbach, C. (2020). SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment.

*Journal of Automated Reasoning*,*64*(3). doi:10.1007/s10817-020-09546-zExport

BibTeX

@article{Teucke2020,
TITLE = {{SPASS-AR}: {A} First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment},
AUTHOR = {Teucke, Andreas and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {0168-7433},
DOI = {10.1007/s10817-020-09546-z},
PUBLISHER = {D. Reidel Pub. Co.},
ADDRESS = {Dordrecht, Holland},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2020},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {64},
NUMBER = {3},
PAGES = {611--640},
}

Endnote

%0 Journal Article
%A Teucke, Andreas
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment :
%G eng
%U http://hdl.handle.net/21.11116/0000-0006-9084-1
%R 10.1007/s10817-020-09546-z
%7 2020
%D 2020
%J Journal of Automated Reasoning
%V 64
%N 3
%& 611
%P 611 - 640
%I D. Reidel Pub. Co.
%C Dordrecht, Holland
%@ false

Voigt, M. (2020). Decidable ∃∗∀∗ First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates.

*Journal of Automated Reasoning*. doi:10.1007/s10817-020-09567-8Export

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 = {2020},
MARGINALMARK = {$\bullet$},
JOURNAL = {Journal of Automated Reasoning},
}

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 2020
%J Journal of Automated Reasoning
%I Springer
%C New York, NY
%@ false

Waldmann, U., Tourret, S., Robillard, S., & Blanchette, J. C. (2020). A Comprehensive Framework for Saturation Theorem Proving. In

*Automated Reasoning (IJCAR 2020)*. Paris, France (Virtual Conference): Springer. doi:10.1007/978-3-030-51074-9_18Export

BibTeX

@inproceedings{Waldmann_IJCAR2020,
TITLE = {A Comprehensive Framework for Saturation Theorem Proving},
AUTHOR = {Waldmann, Uwe and Tourret, Sophie and Robillard, Simon and Blanchette, Jasmin Christian},
LANGUAGE = {eng},
ISBN = {978-3-030-51073-2},
DOI = {10.1007/978-3-030-51074-9_18},
PUBLISHER = {Springer},
YEAR = {2020},
MARGINALMARK = {$\bullet$},
DATE = {2020},
BOOKTITLE = {Automated Reasoning (IJCAR 2020)},
EDITOR = {Peltier, Nicolas and Sofronie-Stokkermans, Viorica},
PAGES = {316--334},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {12166},
ADDRESS = {Paris, France (Virtual Conference)},
}

Endnote

%0 Conference Proceedings
%A Waldmann, Uwe
%A Tourret, Sophie
%A Robillard, Simon
%A Blanchette, Jasmin Christian
%+ 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 A Comprehensive Framework for Saturation Theorem Proving :
%G eng
%U http://hdl.handle.net/21.11116/0000-0007-7971-2
%R 10.1007/978-3-030-51074-9_18
%D 2020
%B 10th International Joint Conference on Automated Reasoning
%Z date of event: 2020-07-01 - 2020-07-04
%C Paris, France (Virtual Conference)
%B Automated Reasoning
%E Peltier, Nicolas; Sofronie-Stokkermans, Viorica
%P 316 - 334
%I Springer
%@ 978-3-030-51073-2
%B Lecture Notes in Artificial Intelligence
%N 12166