# The Year Before Last

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
Bentkamp, A., Blanchette, J. C., Cruanes, S., & Waldmann, U. (2020). Superposition for Lambda-Free Higher-Order Logic. Retrieved from https://arxiv.org/abs/2005.02094
(arXiv: 2005.02094)
Abstract
We introduce refutationally complete superposition calculi for intentional and extensional clausal $\lambda$-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the $\lambda$-free higher-order lexicographic path and Knuth-Bendix orders. We implemented the calculi in the Zipperposition prover and evaluated them on Isabelle/HOL and TPTP benchmarks. They appear promising as a stepping stone towards complete, highly efficient automatic theorem provers for full higher-order logic.
Export
BibTeX
@online{Bentkamp2005.02094, TITLE = {Superposition for Lambda-Free Higher-Order Logic}, AUTHOR = {Bentkamp, Alexander and Blanchette, Jasmin Christian and Cruanes, Simon and Waldmann, Uwe}, LANGUAGE = {eng}, URL = {https://arxiv.org/abs/2005.02094}, EPRINT = {2005.02094}, EPRINTTYPE = {arXiv}, YEAR = {2020}, MARGINALMARK = {$\bullet$}, ABSTRACT = {We introduce refutationally complete superposition calculi for intentional and extensional clausal $\lambda$-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the $\lambda$-free higher-order lexicographic path and Knuth-Bendix orders. We implemented the calculi in the Zipperposition prover and evaluated them on Isabelle/HOL and TPTP benchmarks. They appear promising as a stepping stone towards complete, highly efficient automatic theorem provers for full higher-order logic.}, }
Endnote
%0 Report %A Bentkamp, Alexander %A Blanchette, Jasmin Christian %A Cruanes, Simon %A Waldmann, Uwe %+ External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Superposition for Lambda-Free Higher-Order Logic : %G eng %U http://hdl.handle.net/21.11116/0000-0008-0A5F-4 %U https://arxiv.org/abs/2005.02094 %D 2020 %X We introduce refutationally complete superposition calculi for intentional and extensional clausal $\lambda$-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the $\lambda$-free higher-order lexicographic path and Knuth-Bendix orders. We implemented the calculi in the Zipperposition prover and evaluated them on Isabelle/HOL and TPTP benchmarks. They appear promising as a stepping stone towards complete, highly efficient automatic theorem provers for full higher-order logic. %K Computer Science, Logic in Computer Science, cs.LO,Computer Science, Artificial Intelligence, cs.AI
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&#353;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., 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
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
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_25
Export
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&#246;rg %A Klauck, Michaela %A K&#246;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&#64257;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&#228;t des Saarlandes %C Saarbr&#252;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&#225;cs, Laura %P 212 - 229 %I EasyChair %B EasyChair Proceedings in Computing %N 73 %@ false %U https://easychair.org/publications/paper/b7Cr
Frohn, F. (2020a). A Calculus for Modular Loop Acceleration. Retrieved from https://arxiv.org/abs/2001.01516
(arXiv: 2001.01516)
Abstract
Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs operating on integers. To this end, a variety of acceleration techniques has been proposed. However, all of them are monolithic: Either they accelerate a loop successfully or they fail completely. In contrast, we present a calculus that allows for combining acceleration techniques in a modular way and we show how to integrate many existing acceleration techniques into our calculus. Moreover, we propose two novel acceleration techniques that can be incorporated into our calculus seamlessly. An empirical evaluation demonstrates the applicability of our approach.
Export
BibTeX
@online{Frohn_arXiv2001.01516, TITLE = {A Calculus for Modular Loop Acceleration}, AUTHOR = {Frohn, Florian}, LANGUAGE = {eng}, URL = {https://arxiv.org/abs/2001.01516}, EPRINT = {2001.01516}, EPRINTTYPE = {arXiv}, YEAR = {2020}, MARGINALMARK = {$\bullet$}, ABSTRACT = {Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs operating on integers. To this end, a variety of acceleration techniques has been proposed. However, all of them are monolithic: Either they accelerate a loop successfully or they fail completely. In contrast, we present a calculus that allows for combining acceleration techniques in a modular way and we show how to integrate many existing acceleration techniques into our calculus. Moreover, we propose two novel acceleration techniques that can be incorporated into our calculus seamlessly. An empirical evaluation demonstrates the applicability of our approach.}, }
Endnote
%0 Report %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-CEFC-6 %U https://arxiv.org/abs/2001.01516 %D 2020 %X Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs operating on integers. To this end, a variety of acceleration techniques has been proposed. However, all of them are monolithic: Either they accelerate a loop successfully or they fail completely. In contrast, we present a calculus that allows for combining acceleration techniques in a modular way and we show how to integrate many existing acceleration techniques into our calculus. Moreover, we propose two novel acceleration techniques that can be incorporated into our calculus seamlessly. An empirical evaluation demonstrates the applicability of our approach. %K Computer Science, Logic in Computer Science, cs.LO,Computer Science, Programming Languages, cs.PL
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/3410331
Export
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&#252;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. (2020b). 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_4
Export
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
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
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/nxv1
Export
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&#252;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&#225;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/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. (2020a). Algorithmic Reduction of Biological Networks With Multiple Time Scales. Mathematics in Computer Science, 15. doi:10.1007/s11786-021-00515-2
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 = {2020}, MARGINALMARK = {$\bullet$}, JOURNAL = {Mathematics in Computer Science}, VOLUME = {15}, PAGES = {499--534}, }
Endnote
%0 Journal Article %A Kruff, Niclas %A L&#252;ders, Christoph %A Radulescu, Ovidiu %A Sturm, Thomas %A Walcher, Sebastian %+ External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Algorithmic Reduction of Biological Networks With Multiple Time Scales : %G eng %U http://hdl.handle.net/21.11116/0000-0009-4B0A-9 %R 10.1007/s11786-021-00515-2 %7 2020 %D 2020 %J Mathematics in Computer Science %V 15 %& 499 %P 499 - 534 %I Springer %C New York,NY
Kruff, N., Lüders, C., Radulescu, O., Sturm, T., & Walcher, S. (2020b). 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&#252;ders, Christoph %A Radulescu, Ovidiu %A Sturm, Thomas %A Walcher, Sebastian %+ External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Algorithmic Reduction of Biological Networks With Multiple Time Scales : %G eng %U http://hdl.handle.net/21.11116/0000-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&#231;ois; England, Matthew; Sadykov, Timur M.; Vorozhtsov, Evgenii V. %P 492 - 509 %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
Rahkooy, H., & Sturm, T. (2020a). 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&#231;ois; England, Matthew; Sadykov, Timur M.; Vorozhtsov, Evgenii V. %P 510 - 527 %I Springer %B Lecture Notes in Computer Science %N 12291
Rahkooy, H., & Sturm, T. (2020b). First-Order Tests for Toricity. Retrieved from https://arxiv.org/abs/2002.03586
(arXiv: 2002.03586)
Abstract
Motivated by problems arising with the symbolic analysis of steady state ideals in Chemical Reaction Network Theory, we consider the problem of testing whether the points in a complex or real variety with non-zero coordinates form a coset of a multiplicative group. That property corresponds to Shifted Toricity, a recent generalization of toricity of the corresponding polynomial ideal. The key idea is to take a geometric view on varieties rather than an algebraic view on ideals. Recently, corresponding coset tests have been proposed for complex and for real varieties. The former combine numerous techniques from commutative algorithmic algebra with Gr\"obner bases as the central algorithmic tool. The latter are based on interpreted first-order logic in real closed fields with real quantifier elimination techniques on the algorithmic side. Here we take a new logic approach to both theories, complex and real, and beyond. Besides alternative algorithms, our approach provides a unified view on theories of fields and helps to understand the relevance and interconnection of the rich existing literature in the area, which has been focusing on complex numbers, while from a scientific point of view the (positive) real numbers are clearly the relevant domain in chemical reaction network theory. We apply prototypical implementations of our new approach to a set of 129 models from the BioModels repository.
Export
BibTeX
@online{Rahkooy2002.03586, TITLE = {First-Order Tests for Toricity}, AUTHOR = {Rahkooy, Hamid and Sturm, Thomas}, LANGUAGE = {eng}, URL = {https://arxiv.org/abs/2002.03586}, EPRINT = {2002.03586}, EPRINTTYPE = {arXiv}, YEAR = {2020}, MARGINALMARK = {$\bullet$}, ABSTRACT = {Motivated by problems arising with the symbolic analysis of steady state ideals in Chemical Reaction Network Theory, we consider the problem of testing whether the points in a complex or real variety with non-zero coordinates form a coset of a multiplicative group. That property corresponds to Shifted Toricity, a recent generalization of toricity of the corresponding polynomial ideal. The key idea is to take a geometric view on varieties rather than an algebraic view on ideals. Recently, corresponding coset tests have been proposed for complex and for real varieties. The former combine numerous techniques from commutative algorithmic algebra with Gr\"obner bases as the central algorithmic tool. The latter are based on interpreted first-order logic in real closed fields with real quantifier elimination techniques on the algorithmic side. Here we take a new logic approach to both theories, complex and real, and beyond. Besides alternative algorithms, our approach provides a unified view on theories of fields and helps to understand the relevance and interconnection of the rich existing literature in the area, which has been focusing on complex numbers, while from a scientific point of view the (positive) real numbers are clearly the relevant domain in chemical reaction network theory. We apply prototypical implementations of our new approach to a set of 129 models from the BioModels repository.}, }
Endnote
%0 Report %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-0008-0A76-9 %U https://arxiv.org/abs/2002.03586 %D 2020 %X Motivated by problems arising with the symbolic analysis of steady state ideals in Chemical Reaction Network Theory, we consider the problem of testing whether the points in a complex or real variety with non-zero coordinates form a coset of a multiplicative group. That property corresponds to Shifted Toricity, a recent generalization of toricity of the corresponding polynomial ideal. The key idea is to take a geometric view on varieties rather than an algebraic view on ideals. Recently, corresponding coset tests have been proposed for complex and for real varieties. The former combine numerous techniques from commutative algorithmic algebra with Gr\"obner bases as the central algorithmic tool. The latter are based on interpreted first-order logic in real closed fields with real quantifier elimination techniques on the algorithmic side. Here we take a new logic approach to both theories, complex and real, and beyond. Besides alternative algorithms, our approach provides a unified view on theories of fields and helps to understand the relevance and interconnection of the rich existing literature in the area, which has been focusing on complex numbers, while from a scientific point of view the (positive) real numbers are clearly the relevant domain in chemical reaction network theory. We apply prototypical implementations of our new approach to a set of 129 models from the BioModels repository. %K Computer Science, Symbolic Computation, cs.SC,Quantitative Biology, Molecular Networks, q-bio.MN
Schlichtkrull, A., Blanchette, J. C., Traytel, D., & Waldmann, U. (2020). Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover. Journal of Automated Reasoning, 64. 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$}, DATE = {2020}, JOURNAL = {Journal of Automated Reasoning}, VOLUME = {64}, PAGES = {1169--1195}, }
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 %V 64 %& 1169 %P 1169 - 1195 %I D. Reidel Pub. Co. %C Dordrecht, Holland %@ false
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 &#8707;&#8727;&#8704;&#8727; First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates : %G eng %U http://hdl.handle.net/21.11116/0000-0006-DC7C-8 %R 10.1007/s10817-020-09567-8 %7 2020 %D 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