# Current Year

Barkatou, M. A., Jaroschek, M., & Maddah, S. S. (2017). Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings. Journal of Symbolic Computation, 81. doi:10.1016/j.jsc.2016.11.018
Export
BibTeX
@article{Barkatou2017, TITLE = {Formal Solutions of Completely Integrable {Pfaffian} Systems With Normal Crossings}, AUTHOR = {Barkatou, Moulay A. and Jaroschek, Maximilian and Maddah, Suzy S.}, LANGUAGE = {eng}, ISSN = {0747-7171}, DOI = {10.1016/j.jsc.2016.11.018}, PUBLISHER = {Elsevier}, ADDRESS = {Amsterdam}, YEAR = {2017}, MARGINALMARK = {$\bullet$}, DATE = {2017}, JOURNAL = {Journal of Symbolic Computation}, VOLUME = {81}, PAGES = {41--68}, }
Endnote
%0 Journal Article %A Barkatou, Moulay A. %A Jaroschek, Maximilian %A Maddah, Suzy S. %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-6564-9 %R 10.1016/j.jsc.2016.11.018 %7 2016-11-18 %D 2017 %J Journal of Symbolic Computation %V 81 %& 41 %P 41 - 68 %I Elsevier %C Amsterdam %@ false
Blanchette, J. C., Popescu, A., & Traytel, D. (2017). Soundness and Completeness Proofs by Coinductive Methods. Journal of Automated Reasoning, 58(1). doi:10.1007/s10817-016-9391-3
Export
BibTeX
@article{DBLP:journals/jar/BlanchettePT17, TITLE = {Soundness and Completeness Proofs by Coinductive Methods}, AUTHOR = {Blanchette, Jasmin Christian and Popescu, Andrei and Traytel, Dmitriy}, LANGUAGE = {eng}, ISSN = {0168-7433}, DOI = {10.1007/s10817-016-9391-3}, PUBLISHER = {Springer}, ADDRESS = {London}, YEAR = {2017}, MARGINALMARK = {$\bullet$}, DATE = {2017}, JOURNAL = {Journal of Automated Reasoning}, VOLUME = {58}, NUMBER = {1}, PAGES = {149--179}, }
Endnote
%0 Journal Article %A Blanchette, Jasmin Christian %A Popescu, Andrei %A Traytel, Dmitriy %+ Automation of Logic, MPI for Informatics, Max Planck Society External Organizations External Organizations %T Soundness and Completeness Proofs by Coinductive Methods : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-3B94-0 %R 10.1007/s10817-016-9391-3 %7 2016-10-18 %D 2017 %J Journal of Automated Reasoning %V 58 %N 1 %& 149 %P 149 - 179 %I Springer %C London %@ false
Blanchette, J. C., Waldmann, U., & Wand, D. (2017). A Lambda-Free Higher-Order Recursive Path Order. In Foundations of Software Science and Computation Structures (FoSSaCS 2017). Uppsala, Sweden: Springer. doi:10.1007/978-3-662-54458-7_27
Export
BibTeX
@inproceedings{BlanchetteFoSSaCS2017, TITLE = {A Lambda-Free Higher-Order Recursive Path Order}, AUTHOR = {Blanchette, Jasmin Christian and Waldmann, Uwe and Wand, Daniel}, LANGUAGE = {eng}, ISBN = {978-3-662-54457-0}, DOI = {10.1007/978-3-662-54458-7_27}, PUBLISHER = {Springer}, YEAR = {2017}, MARGINALMARK = {$\bullet$}, DATE = {2017}, BOOKTITLE = {Foundations of Software Science and Computation Structures (FoSSaCS 2017)}, EDITOR = {Esparza, Javier and Murawski, Andrzej S.}, PAGES = {461--479}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {10203}, ADDRESS = {Uppsala, Sweden}, }
Endnote
%0 Conference Proceedings %A Blanchette, Jasmin Christian %A Waldmann, Uwe %A Wand, Daniel %+ 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 A Lambda-Free Higher-Order Recursive Path Order : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002D-91BA-2 %R 10.1007/978-3-662-54458-7_27 %D 2017 %B 20th International Conference on Foundations of Software Science and Computation Structures %Z date of event: 2017-04-24 - 2017-04-27 %C Uppsala, Sweden %B Foundations of Software Science and Computation Structures %E Esparza, Javier; Murawski, Andrzej S. %P 461 - 479 %I Springer %@ 978-3-662-54457-0 %B Lecture Notes in Computer Science %N 10203
Bradford, R., Davenport, J. H., England, M., Errami, H., Gerdt, V., Grigoriev, D., … Weber, A. (2017). A Case Study on the Parametric Occurrence of Multiple Steady States. Retrieved from http://arxiv.org/abs/1704.08997
(arXiv: 1704.08997)
Abstract
We consider the problem of determining multiple steady states for positive real values in models of biological networks. Investigating the potential for these in models of the mitogen-activated protein kinases (MAPK) network has consumed considerable effort using special insights into the structure of corresponding models. Here we apply combinations of symbolic computation methods for mixed equality/inequality systems, specifically virtual substitution, lazy real triangularization and cylindrical algebraic decomposition. We determine multistationarity of an 11-dimensional MAPK network when numeric values are known for all but potentially one parameter. More precisely, our considered model has 11 equations in 11 variables and 19 parameters, 3 of which are of interest for symbolic treatment, and furthermore positivity conditions on all variables and parameters.
Export
BibTeX
@online{DBLP:journals/corr/BradfordDEEGGHK17, TITLE = {A Case Study on the Parametric Occurrence of Multiple Steady States}, 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}, URL = {http://arxiv.org/abs/1704.08997}, EPRINT = {1704.08997}, EPRINTTYPE = {arXiv}, YEAR = {2017}, MARGINALMARK = {$\bullet$}, ABSTRACT = {We consider the problem of determining multiple steady states for positive real values in models of biological networks. Investigating the potential for these in models of the mitogen-activated protein kinases (MAPK) network has consumed considerable effort using special insights into the structure of corresponding models. Here we apply combinations of symbolic computation methods for mixed equality/inequality systems, specifically virtual substitution, lazy real triangularization and cylindrical algebraic decomposition. We determine multistationarity of an 11-dimensional MAPK network when numeric values are known for all but potentially one parameter. More precisely, our considered model has 11 equations in 11 variables and 19 parameters, 3 of which are of interest for symbolic treatment, and furthermore positivity conditions on all variables and parameters.}, }
Endnote
%0 Report %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 A Case Study on the Parametric Occurrence of Multiple Steady States : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002D-91D0-E %U http://arxiv.org/abs/1704.08997 %D 2017 %X We consider the problem of determining multiple steady states for positive real values in models of biological networks. Investigating the potential for these in models of the mitogen-activated protein kinases (MAPK) network has consumed considerable effort using special insights into the structure of corresponding models. Here we apply combinations of symbolic computation methods for mixed equality/inequality systems, specifically virtual substitution, lazy real triangularization and cylindrical algebraic decomposition. We determine multistationarity of an 11-dimensional MAPK network when numeric values are known for all but potentially one parameter. More precisely, our considered model has 11 equations in 11 variables and 19 parameters, 3 of which are of interest for symbolic treatment, and furthermore positivity conditions on all variables and parameters. %K Computer Science, Symbolic Computation, cs.SC
Demri, S., Kapur, D., & Weidenbach, C. (2017). Preface -Special Issue of Selected Extended Papers of IJCAR 2014. Journal of Automated Reasoning, 58(1). doi:10.1007/s10817-016-9394-0
Export
BibTeX
@article{DBLP:journals/jar/DemriKW17, TITLE = {Preface -- Special Issue of Selected Extended Papers of {IJCAR} 2014}, AUTHOR = {Demri, St{\'e}phane and Kapur, Deepak and Weidenbach, Christoph}, LANGUAGE = {eng}, ISSN = {0168-7433}, DOI = {10.1007/s10817-016-9394-0}, PUBLISHER = {D. Reidel Pub. Co.}, ADDRESS = {Dordrecht, Holland}, YEAR = {2017}, MARGINALMARK = {$\bullet$}, DATE = {2017}, JOURNAL = {Journal of Automated Reasoning}, VOLUME = {58}, NUMBER = {1}, PAGES = {1--2}, }
Endnote
%0 Journal Article %A Demri, St&#233;phane %A Kapur, Deepak %A Weidenbach, Christoph %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T Preface -Special Issue of Selected Extended Papers of IJCAR 2014 : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-4CD1-C %R 10.1007/s10817-016-9394-0 %7 2016 %D 2017 %J Journal of Automated Reasoning %V 58 %N 1 %& 1 %P 1 - 2 %I D. Reidel Pub. Co. %C Dordrecht, Holland %@ false
England, M., Errami, H., Grigoriev, D., Radulescu, O., Sturm, T., & Weber, A. (2017). Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks. Retrieved from http://arxiv.org/abs/1706.08794
(arXiv: 1706.08794)
Abstract
We investigate models of the mitogenactivated protein kinases (MAPK) network, with the aim of determining where in parameter space there exist multiple positive steady states. We build on recent progress which combines various symbolic computation methods for mixed systems of equalities and inequalities. We demonstrate that those techniques benefit tremendously from a newly implemented graph theoretical symbolic preprocessing method. We compare computation times and quality of results of numerical continuation methods with our symbolic approach before and after the application of our preprocessing.
Export
BibTeX
@online{DBLP:journals/corr/EnglandEGR0017, TITLE = {Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks}, AUTHOR = {England, Matthew and Errami, Hassan and Grigoriev, Dima and Radulescu, Ovidiu and Sturm, Thomas and Weber, Andreas}, LANGUAGE = {eng}, URL = {http://arxiv.org/abs/1706.08794}, EPRINT = {1706.08794}, EPRINTTYPE = {arXiv}, YEAR = {2017}, MARGINALMARK = {$\bullet$}, ABSTRACT = {We investigate models of the mitogenactivated protein kinases (MAPK) network, with the aim of determining where in parameter space there exist multiple positive steady states. We build on recent progress which combines various symbolic computation methods for mixed systems of equalities and inequalities. We demonstrate that those techniques benefit tremendously from a newly implemented graph theoretical symbolic preprocessing method. We compare computation times and quality of results of numerical continuation methods with our symbolic approach before and after the application of our preprocessing.}, }
Endnote
%0 Report %A England, Matthew %A Errami, Hassan %A Grigoriev, Dima %A Radulescu, Ovidiu %A Sturm, Thomas %A Weber, Andreas %+ External Organizations External Organizations External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002D-91C9-F %U http://arxiv.org/abs/1706.08794 %D 2017 %X We investigate models of the mitogenactivated protein kinases (MAPK) network, with the aim of determining where in parameter space there exist multiple positive steady states. We build on recent progress which combines various symbolic computation methods for mixed systems of equalities and inequalities. We demonstrate that those techniques benefit tremendously from a newly implemented graph theoretical symbolic preprocessing method. We compare computation times and quality of results of numerical continuation methods with our symbolic approach before and after the application of our preprocessing. %K Computer Science, Symbolic Computation, cs.SC
Fontaine, P., Ogawa, M., Sturm, T., & Vu, X. T. (2017). Subtropical Satisfiability. Retrieved from http://arxiv.org/abs/1706.09236
(arXiv: 1706.09236)
Abstract
Quantifier-free nonlinear arithmetic (QF_NRA) appears in many applications of satisfiability modulo theories solving (SMT). Accordingly, efficient reasoning for corresponding constraints in SMT theory solvers is highly relevant. We propose a new incomplete but efficient and terminating method to identify satisfiable instances. The method is derived from the subtropical method recently introduced in the context of symbolic computation for computing real zeros of single very large multivariate polynomials. Our method takes as input conjunctions of strict polynomial inequalities, which represent more than 40% of the QF_NRA section of the SMT-LIB library of benchmarks. The method takes an abstraction of polynomials as exponent vectors over the natural numbers tagged with the signs of the corresponding coefficients. It then uses, in turn, SMT to solve linear problems over the reals to heuristically find suitable points that translate back to satisfying points for the original problem. Systematic experiments on the SMT-LIB demonstrate that our method is not a sufficiently strong decision procedure by itself but a valuable heuristic to use within a portfolio of techniques.
Export
BibTeX
@online{DBLP:journals/corr/FontaineO0V17, TITLE = {Subtropical Satisfiability}, AUTHOR = {Fontaine, Pascal and Ogawa, Mizuhito and Sturm, Thomas and Vu, Xuan Tung}, LANGUAGE = {eng}, URL = {http://arxiv.org/abs/1706.09236}, EPRINT = {1706.09236}, EPRINTTYPE = {arXiv}, YEAR = {2017}, MARGINALMARK = {$\bullet$}, ABSTRACT = {Quantifier-free nonlinear arithmetic (QF_NRA) appears in many applications of satisfiability modulo theories solving (SMT). Accordingly, efficient reasoning for corresponding constraints in SMT theory solvers is highly relevant. We propose a new incomplete but efficient and terminating method to identify satisfiable instances. The method is derived from the subtropical method recently introduced in the context of symbolic computation for computing real zeros of single very large multivariate polynomials. Our method takes as input conjunctions of strict polynomial inequalities, which represent more than 40% of the QF_NRA section of the SMT-LIB library of benchmarks. The method takes an abstraction of polynomials as exponent vectors over the natural numbers tagged with the signs of the corresponding coefficients. It then uses, in turn, SMT to solve linear problems over the reals to heuristically find suitable points that translate back to satisfying points for the original problem. Systematic experiments on the SMT-LIB demonstrate that our method is not a sufficiently strong decision procedure by itself but a valuable heuristic to use within a portfolio of techniques.}, }
Endnote
%0 Report %A Fontaine, Pascal %A Ogawa, Mizuhito %A Sturm, Thomas %A Vu, Xuan Tung %+ External Organizations External Organizations Automation of Logic, MPI for Informatics, Max Planck Society External Organizations %T Subtropical Satisfiability : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002D-91C2-E %U http://arxiv.org/abs/1706.09236 %D 2017 %X Quantifier-free nonlinear arithmetic (QF_NRA) appears in many applications of satisfiability modulo theories solving (SMT). Accordingly, efficient reasoning for corresponding constraints in SMT theory solvers is highly relevant. We propose a new incomplete but efficient and terminating method to identify satisfiable instances. The method is derived from the subtropical method recently introduced in the context of symbolic computation for computing real zeros of single very large multivariate polynomials. Our method takes as input conjunctions of strict polynomial inequalities, which represent more than 40% of the QF_NRA section of the SMT-LIB library of benchmarks. The method takes an abstraction of polynomials as exponent vectors over the natural numbers tagged with the signs of the corresponding coefficients. It then uses, in turn, SMT to solve linear problems over the reals to heuristically find suitable points that translate back to satisfying points for the original problem. Systematic experiments on the SMT-LIB demonstrate that our method is not a sufficiently strong decision procedure by itself but a valuable heuristic to use within a portfolio of techniques. %K Computer Science, Logic in Computer Science, cs.LO
Horbach, M., Voigt, M., & Weidenbach, C. (2017a). On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. Retrieved from http://arxiv.org/abs/1705.08792
(arXiv: 1705.08792)
Abstract
In general, first-order predicate logic extended with linear integer arithmetic is undecidable. We show that the Bernays-Sch\"onfinkel-Ramsey fragment ($\exists^* \forall^*$-sentences) extended with a restricted form of linear integer arithmetic is decidable via finite ground instantiation. The identified ground instances can be employed to restrict the search space of existing automated reasoning procedures considerably, e.g., when reasoning about quantified properties of array data structures formalized in Bradley, Manna, and Sipma's array property fragment. Typically, decision procedures for the array property fragment are based on an exhaustive instantiation of universally quantified array indices with all the ground index terms that occur in the formula at hand. Our results reveal that one can get along with significantly fewer instances.
Export
BibTeX
@online{HorbachArXiv2017, TITLE = {On the Combination of the Bernays-Sch{\"o}nfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic}, AUTHOR = {Horbach, Matthias and Voigt, Marco and Weidenbach, Christoph}, LANGUAGE = {eng}, URL = {http://arxiv.org/abs/1705.08792}, EPRINT = {1705.08792}, EPRINTTYPE = {arXiv}, YEAR = {2017}, MARGINALMARK = {$\bullet$}, ABSTRACT = {In general, first-order predicate logic extended with linear integer arithmetic is undecidable. We show that the Bernays-Sch\"onfinkel-Ramsey fragment ($\exists^* \forall^*$-sentences) extended with a restricted form of linear integer arithmetic is decidable via finite ground instantiation. The identified ground instances can be employed to restrict the search space of existing automated reasoning procedures considerably, e.g., when reasoning about quantified properties of array data structures formalized in Bradley, Manna, and Sipma's array property fragment. Typically, decision procedures for the array property fragment are based on an exhaustive instantiation of universally quantified array indices with all the ground index terms that occur in the formula at hand. Our results reveal that one can get along with significantly fewer instances.}, }
Endnote
%0 Report %A Horbach, Matthias %A Voigt, Marco %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 On the Combination of the Bernays-Sch&#246;nfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002D-8140-2 %U http://arxiv.org/abs/1705.08792 %D 2017 %X In general, first-order predicate logic extended with linear integer arithmetic is undecidable. We show that the Bernays-Sch\"onfinkel-Ramsey fragment ($\exists^* \forall^*$-sentences) extended with a restricted form of linear integer arithmetic is decidable via finite ground instantiation. The identified ground instances can be employed to restrict the search space of existing automated reasoning procedures considerably, e.g., when reasoning about quantified properties of array data structures formalized in Bradley, Manna, and Sipma's array property fragment. Typically, decision procedures for the array property fragment are based on an exhaustive instantiation of universally quantified array indices with all the ground index terms that occur in the formula at hand. Our results reveal that one can get along with significantly fewer instances. %K Computer Science, Logic in Computer Science, cs.LO
Horbach, M., Voigt, M., & Weidenbach, C. (2017b). The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable. Retrieved from http://arxiv.org/abs/1703.01212
(arXiv: 1703.01212)
Abstract
The first-order theory of addition over the natural numbers, known as Presburger arithmetic, is decidable in double exponential time. Adding an uninterpreted unary predicate to the language leads to an undecidable theory. We sharpen the known boundary between decidable and undecidable in that we show that the purely universal fragment of the extended theory is already undecidable. Our proof is based on a reduction of the halting problem for two-counter machines to unsatisfiability of sentences in the extended language of Presburger arithmetic that does not use existential quantification. On the other hand, we argue that a single $\forall\exists$ quantifier alternation turns the set of satisfiable sentences of the extended language into a $\Sigma^1_1$-complete set. Some of the mentioned results can be transfered to the realm of linear arithmetic over the ordered real numbers. This concerns the undecidability of the purely universal fragment and the $\Sigma^1_1$-hardness for sentences with at least one quantifier alternation. Finally, we discuss the relevance of our results to verification. In particular, we derive undecidability results for quantified fragments of separation logic, the theory of arrays, and combinations of the theory of equality over uninterpreted functions with restricted forms of integer arithmetic. In certain cases our results even imply the absence of sound and complete deductive calculi.
Export
BibTeX
@online{VoigtHorbachWeidenbacharXiv2017, TITLE = {The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable}, AUTHOR = {Horbach, Matthias and Voigt, Marco and Weidenbach, Christoph}, LANGUAGE = {eng}, URL = {http://arxiv.org/abs/1703.01212}, EPRINT = {1703.01212}, EPRINTTYPE = {arXiv}, YEAR = {2017}, MARGINALMARK = {$\bullet$}, ABSTRACT = {The first-order theory of addition over the natural numbers, known as Presburger arithmetic, is decidable in double exponential time. Adding an uninterpreted unary predicate to the language leads to an undecidable theory. We sharpen the known boundary between decidable and undecidable in that we show that the purely universal fragment of the extended theory is already undecidable. Our proof is based on a reduction of the halting problem for two-counter machines to unsatisfiability of sentences in the extended language of Presburger arithmetic that does not use existential quantification. On the other hand, we argue that a single $\forall\exists$ quantifier alternation turns the set of satisfiable sentences of the extended language into a $\Sigma^1_1$-complete set. Some of the mentioned results can be transfered to the realm of linear arithmetic over the ordered real numbers. This concerns the undecidability of the purely universal fragment and the $\Sigma^1_1$-hardness for sentences with at least one quantifier alternation. Finally, we discuss the relevance of our results to verification. In particular, we derive undecidability results for quantified fragments of separation logic, the theory of arrays, and combinations of the theory of equality over uninterpreted functions with restricted forms of integer arithmetic. In certain cases our results even imply the absence of sound and complete deductive calculi.}, }
Endnote
%0 Report %A Horbach, Matthias %A Voigt, Marco %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 The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-A5E7-D %U http://arxiv.org/abs/1703.01212 %D 2017 %X The first-order theory of addition over the natural numbers, known as Presburger arithmetic, is decidable in double exponential time. Adding an uninterpreted unary predicate to the language leads to an undecidable theory. We sharpen the known boundary between decidable and undecidable in that we show that the purely universal fragment of the extended theory is already undecidable. Our proof is based on a reduction of the halting problem for two-counter machines to unsatisfiability of sentences in the extended language of Presburger arithmetic that does not use existential quantification. On the other hand, we argue that a single $\forall\exists$ quantifier alternation turns the set of satisfiable sentences of the extended language into a $\Sigma^1_1$-complete set. Some of the mentioned results can be transfered to the realm of linear arithmetic over the ordered real numbers. This concerns the undecidability of the purely universal fragment and the $\Sigma^1_1$-hardness for sentences with at least one quantifier alternation. Finally, we discuss the relevance of our results to verification. In particular, we derive undecidability results for quantified fragments of separation logic, the theory of arrays, and combinations of the theory of equality over uninterpreted functions with restricted forms of integer arithmetic. In certain cases our results even imply the absence of sound and complete deductive calculi. %K Computer Science, Logic in Computer Science, cs.LO
Lamotte-Schubert, M., & Weidenbach, C. (2017). BDI: A New Decidable Clause Class. Journal of Logic and Computation, 27(2). doi:10.1093/logcom/exu074
Export
BibTeX
@article{Lamotte-SchubertWeidenbach13a, TITLE = {{BDI}: A New Decidable Clause Class}, AUTHOR = {Lamotte-Schubert, Manuel and Weidenbach, Christoph}, LANGUAGE = {eng}, ISSN = {0955-792X}, DOI = {10.1093/logcom/exu074}, PUBLISHER = {Oxford University Press}, ADDRESS = {Oxford}, YEAR = {2017}, MARGINALMARK = {$\bullet$}, DATE = {2017}, JOURNAL = {Journal of Logic and Computation}, VOLUME = {27}, NUMBER = {2}, PAGES = {441--468}, }
Endnote
%0 Journal Article %A Lamotte-Schubert, Manuel %A Weidenbach, Christoph %+ Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T BDI: A New Decidable Clause Class : %G eng %U http://hdl.handle.net/11858/00-001M-0000-0024-C365-F %R 10.1093/logcom/exu074 %7 2014-12-08 %D 2017 %J Journal of Logic and Computation %V 27 %N 2 %& 441 %P 441 - 468 %I Oxford University Press %C Oxford %@ false %U https://hal.inria.fr/hal-01098084
Reynolds, A., & Blanchette, J. C. (2017). A Decision Procedure for (Co)datatypes in SMT Solvers. Journal of Automated Reasoning, 58(3). doi:10.1007/s10817-016-9372-6
Export
BibTeX
@article{DBLP:journals/jar/ReynoldsB17, TITLE = {A Decision Procedure for (Co)datatypes in {SMT} Solvers}, AUTHOR = {Reynolds, Andrew and Blanchette, Jasmin Christian}, LANGUAGE = {eng}, ISSN = {0168-7433}, DOI = {10.1007/s10817-016-9372-6}, PUBLISHER = {Springer}, ADDRESS = {New York, NY}, YEAR = {2017}, MARGINALMARK = {$\bullet$}, DATE = {2017}, JOURNAL = {Journal of Automated Reasoning}, EDITOR = {Kambhampati, Subbarao}, VOLUME = {58}, NUMBER = {3}, PAGES = {341--362}, }
Endnote
%0 Journal Article %A Reynolds, Andrew %A Blanchette, Jasmin Christian %+ External Organizations Automation of Logic, MPI for Informatics, Max Planck Society %T A Decision Procedure for (Co)datatypes in SMT Solvers : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-80D4-C %R 10.1007/s10817-016-9372-6 %7 2017 %D 2017 %J Journal of Automated Reasoning %V 58 %N 3 %& 341 %P 341 - 362 %I Springer %C New York, NY %@ false
Sturm, T. (n.d.). A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications. Mathematics in Computer Science.
(Accepted/in press)
Export
BibTeX
@article{Sturm2017, TITLE = {A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications}, AUTHOR = {Sturm, Thomas}, LANGUAGE = {eng}, PUBLISHER = {Springer}, ADDRESS = {New York, NY}, YEAR = {2017}, PUBLREMARK = {Accepted}, MARGINALMARK = {$\bullet$}, JOURNAL = {Mathematics in Computer Science}, }
Endnote
%0 Journal Article %A Sturm, Thomas %+ Automation of Logic, MPI for Informatics, Max Planck Society %T A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-A3B5-B %D 2017 %J Mathematics in Computer Science %I Springer %C New York, NY
Teucke, A., & Weidenbach, C. (2017). Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. Retrieved from http://arxiv.org/abs/1703.02837
(arXiv: 1703.02837)
Abstract
The monadic shallow linear Horn fragment is well-known to be decidable and has many application, e.g., in security protocol analysis, tree automata, or abstraction refinement. It was a long standing open problem how to extend the fragment to the non-Horn case, preserving decidability, that would, e.g., enable to express non-determinism in protocols. We prove decidability of the non-Horn monadic shallow linear fragment via ordered resolution further extended with dismatching constraints and discuss some applications of the new decidable fragment.
Export
BibTeX
@online{TeuckearXiv2017, TITLE = {Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints}, AUTHOR = {Teucke, Andreas and Weidenbach, Christoph}, LANGUAGE = {eng}, URL = {http://arxiv.org/abs/1703.02837}, EPRINT = {1703.02837}, EPRINTTYPE = {arXiv}, YEAR = {2017}, MARGINALMARK = {$\bullet$}, ABSTRACT = {The monadic shallow linear Horn fragment is well-known to be decidable and has many application, e.g., in security protocol analysis, tree automata, or abstraction refinement. It was a long standing open problem how to extend the fragment to the non-Horn case, preserving decidability, that would, e.g., enable to express non-determinism in protocols. We prove decidability of the non-Horn monadic shallow linear fragment via ordered resolution further extended with dismatching constraints and discuss some applications of the new decidable fragment.}, }
Endnote
%0 Report %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 Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-A213-1 %U http://arxiv.org/abs/1703.02837 %D 2017 %X The monadic shallow linear Horn fragment is well-known to be decidable and has many application, e.g., in security protocol analysis, tree automata, or abstraction refinement. It was a long standing open problem how to extend the fragment to the non-Horn case, preserving decidability, that would, e.g., enable to express non-determinism in protocols. We prove decidability of the non-Horn monadic shallow linear fragment via ordered resolution further extended with dismatching constraints and discuss some applications of the new decidable fragment. %K Computer Science, Logic in Computer Science, cs.LO
Voigt, M. (n.d.). A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment. In Proceedings of the 32nd Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2017). Reykjavik, Island: ACM.
(Accepted/in press)
Export
BibTeX
@inproceedings{VoigtLICS2017, TITLE = {A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment}, AUTHOR = {Voigt, Marco}, LANGUAGE = {eng}, PUBLISHER = {ACM}, YEAR = {2017}, PUBLREMARK = {Accepted}, MARGINALMARK = {$\bullet$}, BOOKTITLE = {Proceedings of the 32nd Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2017)}, ADDRESS = {Reykjavik, Island}, }
Endnote
%0 Conference Proceedings %A Voigt, Marco %+ Automation of Logic, MPI for Informatics, Max Planck Society %T A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002C-EFA6-4 %D 2017 %B 32nd Annual ACM-IEEE Symposium on Logic in Computer Science %Z date of event: 2017-06-20 - 2017-06-23 %C Reykjavik, Island %B Proceedings of the 32nd Annual ACM-IEEE Symposium on Logic in Computer Science %I ACM
Voigt, M. (2017). A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment. Retrieved from http://arxiv.org/abs/1704.02145
(arXiv: 1704.02145)
Abstract
Recently, the separated fragment (SF) has been introduced and proved to be decidable. Its defining principle is that universally and existentially quantified variables may not occur together in atoms. The known upper bound on the time required to decide SF's satisfiability problem is formulated in terms of quantifier alternations: Given an SF sentence $\exists \vec{z} \forall \vec{x}_1 \exists \vec{y}_1 \ldots \forall \vec{x}_n \exists \vec{y}_n . \psi$ in which $\psi$ is quantifier free, satisfiability can be decided in nondeterministic $n$-fold exponential time. In the present paper, we conduct a more fine-grained analysis of the complexity of SF-satisfiability. We derive an upper and a lower bound in terms of the degree of interaction of existential variables (short: degree)}---a novel measure of how many separate existential quantifier blocks in a sentence are connected via joint occurrences of variables in atoms. Our main result is the $k$-NEXPTIME-completeness of the satisfiability problem for the set $SF_{\leq k}$ of all SF sentences that have degree $k$ or smaller. Consequently, we show that SF-satisfiability is non-elementary in general, since SF is defined without restrictions on the degree. Beyond trivial lower bounds, nothing has been known about the hardness of SF-satisfiability so far.
Export
BibTeX
@online{VoigtLICS2017ArxivFullPaper, TITLE = {A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment}, AUTHOR = {Voigt, Marco}, URL = {http://arxiv.org/abs/1704.02145}, EPRINT = {1704.02145}, EPRINTTYPE = {arXiv}, YEAR = {2017}, MARGINALMARK = {$\bullet$}, ABSTRACT = {Recently, the separated fragment (SF) has been introduced and proved to be decidable. Its defining principle is that universally and existentially quantified variables may not occur together in atoms. The known upper bound on the time required to decide SF's satisfiability problem is formulated in terms of quantifier alternations: Given an SF sentence $\exists \vec{z} \forall \vec{x}_1 \exists \vec{y}_1 \ldots \forall \vec{x}_n \exists \vec{y}_n . \psi$ in which $\psi$ is quantifier free, satisfiability can be decided in nondeterministic $n$-fold exponential time. In the present paper, we conduct a more fine-grained analysis of the complexity of SF-satisfiability. We derive an upper and a lower bound in terms of the degree of interaction of existential variables (short: degree)}---a novel measure of how many separate existential quantifier blocks in a sentence are connected via joint occurrences of variables in atoms. Our main result is the $k$-NEXPTIME-completeness of the satisfiability problem for the set $SF_{\leq k}$ of all SF sentences that have degree $k$ or smaller. Consequently, we show that SF-satisfiability is non-elementary in general, since SF is defined without restrictions on the degree. Beyond trivial lower bounds, nothing has been known about the hardness of SF-satisfiability so far.}, }
Endnote
%0 Report %A Voigt, Marco %+ Automation of Logic, MPI for Informatics, Max Planck Society %T A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment : %U http://hdl.handle.net/11858/00-001M-0000-002C-EFA0-0 %U http://arxiv.org/abs/1704.02145 %D 2017 %X Recently, the separated fragment (SF) has been introduced and proved to be decidable. Its defining principle is that universally and existentially quantified variables may not occur together in atoms. The known upper bound on the time required to decide SF's satisfiability problem is formulated in terms of quantifier alternations: Given an SF sentence $\exists \vec{z} \forall \vec{x}_1 \exists \vec{y}_1 \ldots \forall \vec{x}_n \exists \vec{y}_n . \psi$ in which $\psi$ is quantifier free, satisfiability can be decided in nondeterministic $n$-fold exponential time. In the present paper, we conduct a more fine-grained analysis of the complexity of SF-satisfiability. We derive an upper and a lower bound in terms of the degree of interaction of existential variables (short: degree)}---a novel measure of how many separate existential quantifier blocks in a sentence are connected via joint occurrences of variables in atoms. Our main result is the $k$-NEXPTIME-completeness of the satisfiability problem for the set $SF_{\leq k}$ of all SF sentences that have degree $k$ or smaller. Consequently, we show that SF-satisfiability is non-elementary in general, since SF is defined without restrictions on the degree. Beyond trivial lower bounds, nothing has been known about the hardness of SF-satisfiability so far. %K Computer Science, Logic in Computer Science, cs.LO
Wand, D., Weidenbach, C., Blanchette, J. C., & Sutcliffe, G. (2017). Superposition: Types and Induction. Universität des Saarlandes, Saarbürkcne. Retrieved from urn:nbn:de:bsz:291-scidok-69522
Abstract
Proof assistants are becoming widespread for formalization of theories both in computer science and mathematics. They provide rich logics with powerful type systems and machine-checked proofs which increase the confidence in the correctness in complicated and detailed proofs. However, they incur a significant overhead compared to pen-and-paper proofs. This thesis describes work on bridging the gap between high-order proof assistants and first-order automated theorem provers by extending the capabilities of the automated theorem provers to provide features usually found in proof assistants. My first contribution is the development and implementation of a first-order superposition calculus with a polymorphic type system that supports type classes and the accompanying refutational completeness proof for that calculus. The inclusion of the type system into the superposition calculus and solvers completely removes the type encoding overhead when encoding problems from many proof assistants. My second contribution is the development of SupInd, an extension of the typed superposition calculus that supports data types and structural induction over those data types. It includes heuristics that guide the induction and conjecture strengthening techniques, which can be applied independently of the underlying calculus. I have implemented the contributions in a tool called Pirate. The evaluations of both contributions show promising results.
Export
BibTeX
@phdthesis{wandphd2017, TITLE = {Superposition: Types and Induction}, AUTHOR = {Wand, Daniel and Weidenbach, Christoph and Blanchette, Jasmin Christian and Sutcliffe, Geoff}, LANGUAGE = {eng}, URL = {urn:nbn:de:bsz:291-scidok-69522}, SCHOOL = {Universit{\"a}t des Saarlandes}, ADDRESS = {Saarb{\"u}rkcne}, YEAR = {2017}, MARGINALMARK = {$\bullet$}, DATE = {2017}, ABSTRACT = {Proof assistants are becoming widespread for formalization of theories both in computer science and mathematics. They provide rich logics with powerful type systems and machine-checked proofs which increase the confidence in the correctness in complicated and detailed proofs. However, they incur a significant overhead compared to pen-and-paper proofs. This thesis describes work on bridging the gap between high-order proof assistants and first-order automated theorem provers by extending the capabilities of the automated theorem provers to provide features usually found in proof assistants. My first contribution is the development and implementation of a first-order superposition calculus with a polymorphic type system that supports type classes and the accompanying refutational completeness proof for that calculus. The inclusion of the type system into the superposition calculus and solvers completely removes the type encoding overhead when encoding problems from many proof assistants. My second contribution is the development of SupInd, an extension of the typed superposition calculus that supports data types and structural induction over those data types. It includes heuristics that guide the induction and conjecture strengthening techniques, which can be applied independently of the underlying calculus. I have implemented the contributions in a tool called Pirate. The evaluations of both contributions show promising results.}, }
Endnote
%0 Thesis %A Wand, Daniel %A Weidenbach, Christoph %A Blanchette, Jasmin Christian %A Sutcliffe, Geoff %+ 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 Automation of Logic, MPI for Informatics, Max Planck Society Automation of Logic, MPI for Informatics, Max Planck Society %T Superposition: Types and Induction : %G eng %U http://hdl.handle.net/11858/00-001M-0000-002D-E99C-5 %U urn:nbn:de:bsz:291-scidok-69522 %I Universit&#228;t des Saarlandes %C Saarb&#252;rkcne %D 2017 %P x, 167 p. %V phd %9 phd %X Proof assistants are becoming widespread for formalization of theories both in computer science and mathematics. They provide rich logics with powerful type systems and machine-checked proofs which increase the confidence in the correctness in complicated and detailed proofs. However, they incur a significant overhead compared to pen-and-paper proofs. This thesis describes work on bridging the gap between high-order proof assistants and first-order automated theorem provers by extending the capabilities of the automated theorem provers to provide features usually found in proof assistants. My first contribution is the development and implementation of a first-order superposition calculus with a polymorphic type system that supports type classes and the accompanying refutational completeness proof for that calculus. The inclusion of the type system into the superposition calculus and solvers completely removes the type encoding overhead when encoding problems from many proof assistants. My second contribution is the development of SupInd, an extension of the typed superposition calculus that supports data types and structural induction over those data types. It includes heuristics that guide the induction and conjecture strengthening techniques, which can be applied independently of the underlying calculus. I have implemented the contributions in a tool called Pirate. The evaluations of both contributions show promising results. %U http://scidok.sulb.uni-saarland.de/volltexte/2017/6952/http://scidok.sulb.uni-saarland.de/doku/lic_ohne_pod.php?la=de