• Moulay A. Barkatou, Maximilian Jaroschek, and Suzy S. Maddah, "Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings," Journal of Symbolic Computation 81, 41-68 (2017).
Citation
Moulay A. Barkatou, Maximilian Jaroschek, and Suzy S. Maddah, "Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings," Journal of Symbolic Computation 81, 41-68 (2017).
Export
• Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel, "Soundness and Completeness Proofs by Coinductive Methods," Journal of Automated Reasoning 58 (1), 149-179 (2017).
Citation
Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel, "Soundness and Completeness Proofs by Coinductive Methods," Journal of Automated Reasoning 58 (1), 149-179 (2017).
Export
• Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, "Preface -Special Issue of Selected Extended Papers of IJCAR 2014," Journal of Automated Reasoning 58 (1), 1-2 (2017).
Citation
Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, "Preface -Special Issue of Selected Extended Papers of IJCAR 2014," Journal of Automated Reasoning 58 (1), 1-2 (2017).
Export
• Matthias Horbach, Marco Voigt, and Christoph Weidenbach, "The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable", (2017), pp. 22 p.
Citation
Matthias Horbach, Marco Voigt, and Christoph Weidenbach, "The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable", (2017), pp. 22 p.
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
• Manuel Lamotte-Schubert and Christoph Weidenbach, "BDI: A New Decidable Clause Class," Journal of Logic and Computation 27 (2), 441-468 (2017).
Citation
Manuel Lamotte-Schubert and Christoph Weidenbach, "BDI: A New Decidable Clause Class," Journal of Logic and Computation 27 (2), 441-468 (2017).
Export
• Andrew Reynolds and Jasmin Christian Blanchette, "A Decision Procedure for (Co)datatypes in SMT Solvers," Journal of Automated Reasoning 58 (3), 341-362 (2017).
Citation
Andrew Reynolds and Jasmin Christian Blanchette, "A Decision Procedure for (Co)datatypes in SMT Solvers," Journal of Automated Reasoning 58 (3), 341-362 (2017).
Export
• Andreas Teucke and Christoph Weidenbach, "Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints", (2017), pp. 28 p.
Citation
Andreas Teucke and Christoph Weidenbach, "Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints", (2017), pp. 28 p.
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
• Marco Voigt, "A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment", (2017), pp. 38 p.
Citation
Marco Voigt, "A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment", (2017), pp. 38 p.
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