Current 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-y
Export
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-1
Export
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.008
Export
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.021
Export
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
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.017
Export
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-y
Export
BibTeX
@article{Eingland2020,
TITLE = {Foreword, with a Dedication to {Andreas Weber}},
AUTHOR = {England, Matthew and Koepf, Wolfram and Sadykov, Timor and Seiler, Werner M. and Sturm, Thomas},
LANGUAGE = {eng},
ISSN = {1661-8270},
DOI = {10.1007/s11786-020-00476-y},
PUBLISHER = {Springer},
ADDRESS = {New York, NY},
YEAR = {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
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/96wb
Export
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
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-9
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 = {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-4
Export
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
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/59
Export
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_29
Export
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_30
Export
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
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-0
Export
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-x
Export
BibTeX
@article{Seiler2020,
TITLE = {A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations},
AUTHOR = {Seiler, Werner M. and Sei{\ss}, Matthias and Sturm, Thomas},
LANGUAGE = {eng},
ISSN = {1661-8270},
DOI = {10.1007/s11786-020-00485-x},
PUBLISHER = {Springer},
ADDRESS = {New York, NY},
YEAR = {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-z
Export
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-8
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 = {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_18
Export
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