• Gábor Alagi and Christoph Weidenbach, "NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment ", (2015), pp. 43 p.  
    Citation
    Gábor Alagi and Christoph Weidenbach, "NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment ", (2015), pp. 43 p.
    Abstract
    We combine key ideas from first-order superposition and propositional CDCL to create the new calculus NRCL deciding the Bernays-Sch\"onfinkel fragment. It inherits the abstract redundancy criterion and the monotone model operator from superposition. CDCL adds to NRCL the dynamic, conflict-driven search for an atom ordering inducing a model. As a result, in NRCL a false clause can be effectively found modulo the current model assumption. It guides the derivation of a first-order ordered resolvent that is never redundant. Similar to 1UIP-learning in CDCL, the learned resolvent induces backtracking and via propagation blocks the previous conflict state for the rest of the search. Since learned clauses are never redundant, only finitely many can be generated by NRCL on the Bernays-Sch\"onfinkel fragment, which provides a nice argument for termination.
    Export
  • Gábor Alagi and Christoph Weidenbach, "NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 69-84.  
    Citation
    Gábor Alagi and Christoph Weidenbach, "NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 69-84.
    Export
  • Moulay A. Barkatou, Maximilian Jaroschek, and Suzy S. Maddah, "Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings", (2015), pp. 31 p.  
    Citation
    Moulay A. Barkatou, Maximilian Jaroschek, and Suzy S. Maddah, "Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings", (2015), pp. 31 p.
    Abstract
    In this paper, we present an algorithm for computing a fundamental matrix of formal solutions of completely integrable Pfaffian systems with normal crossings in several variables. This algorithm is a generalization of a method developed for the bivariate case based on a combination of several reduction techniques and is implemented in the computer algebra system Maple.
    Export
  • Peter Baumgartner, Joshua Bax, and Uwe Waldmann, "Beagle -- A Hierarchic Superposition Theorem Prover", in Automated Deduction -- CADE-25, edited by Amy P. Felty and Aart Middeldorp (Springer, Berlin, 2015), pp. 367-377.  
    Citation
    Peter Baumgartner, Joshua Bax, and Uwe Waldmann, "Beagle -- A Hierarchic Superposition Theorem Prover", in Automated Deduction -- CADE-25, edited by Amy P. Felty and Aart Middeldorp (Springer, Berlin, 2015), pp. 367-377.
    Export
  • Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel, "Witnessing (Co)datatypes", in Programming Languages and Systems, edited by Jan Vitek (Springer, Berlin, 2015), pp. 359-382.  
    Citation
    Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel, "Witnessing (Co)datatypes", in Programming Languages and Systems, edited by Jan Vitek (Springer, Berlin, 2015), pp. 359-382.
    Export
  • Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, and Tobias Nipkow, "Mining the Archive of Formal Proofs", in Intelligent Computer Mathematics, edited by Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge (Springer, Berlin, 2015), pp. 3-17.  
    Citation
    Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, and Tobias Nipkow, "Mining the Archive of Formal Proofs", in Intelligent Computer Mathematics, edited by Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge (Springer, Berlin, 2015), pp. 3-17.
    Export
  • Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel, "Foundational Extensible Corecursion", (2015), pp. 12 p.  
    Citation
    Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel, "Foundational Extensible Corecursion", (2015), pp. 12 p.
    Abstract
    This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to and relational parametricity. The end product is a general corecursor that allows corecursive (and even recursive) calls under well-behaved operations, including constructors. Corecursive functions that are well behaved can be registered as such, thereby increasing the corecursor's expressiveness. The metatheory is formalized in the Isabelle proof assistant and forms the core of a prototype tool. The corecursor is derived from first principles, without requiring new axioms or extensions of the logic.
    Export
  • Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel, "Foundational Extensible Corecursion: A Proof Assistant Perspective", in Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, (ACM, New York, NY, 2015), pp. 192-204.  
    Citation
    Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel, "Foundational Extensible Corecursion: A Proof Assistant Perspective", in Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, (ACM, New York, NY, 2015), pp. 192-204.
    Export
  • Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier, "Semi-intelligible Isar Proofs from Machine-Generated Proofs," Journal of Automated Reasoning 56 (2), 155-200 (2016).  
    Citation
    Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier, "Semi-intelligible Isar Proofs from Machine-Generated Proofs," Journal of Automated Reasoning 56 (2), 155-200 (2016).
    Export
  • Jasmin Christian Blanchette and Nikolai Kosmatov (eds), Tests and Proofs. (Springer, Berlin, 2015).  
    Citation
    Jasmin Christian Blanchette and Nikolai Kosmatov (eds), Tests and Proofs. (Springer, Berlin, 2015).
    Export
  • Martin Bromberger, Thomas Sturm, and Christoph Weidenbach, "Linear Integer Arithmetic Revisited", (2015), pp. 34 p.  
    Citation
    Martin Bromberger, Thomas Sturm, and Christoph Weidenbach, "Linear Integer Arithmetic Revisited", (2015), pp. 34 p.
    Abstract
    We consider feasibility of linear integer programs in the context of verification systems such as SMT solvers or theorem provers. Although satisfiability of linear integer programs is decidable, many state-of-the-art solvers neglect termination in favor of efficiency. It is challenging to design a solver that is both terminating and practically efficient. Recent work by Jovanovic and de Moura constitutes an important step into this direction. Their algorithm CUTSAT is sound, but does not terminate, in general. In this paper we extend their CUTSAT algorithm by refined inference rules, a new type of conflicting core, and a dedicated rule application strategy. This leads to our algorithm CUTSAT++, which guarantees termination.
    Export
  • Martin Bromberger, Thomas Sturm, and Christoph Weidenbach, "Linear Integer Arithmetic Revisited", in Automated Deduction -- CADE-25, edited by Amy P. Felty and Aart Middeldorp (Springer, Berlin, 2015), pp. 623-637.  
    Citation
    Martin Bromberger, Thomas Sturm, and Christoph Weidenbach, "Linear Integer Arithmetic Revisited", in Automated Deduction -- CADE-25, edited by Amy P. Felty and Aart Middeldorp (Springer, Berlin, 2015), pp. 623-637.
    Export
  • Christopher W. Brown and Marek Košta, "Constructing a Single Cell in Cylindrical Algebraic Decomposition," Journal of Symbolic Computation 70, 14-48 (2015).  
    Citation
    Christopher W. Brown and Marek Košta, "Constructing a Single Cell in Cylindrical Algebraic Decomposition," Journal of Symbolic Computation 70, 14-48 (2015).
    Export
  • Werner Damm, Matthias Horbach, and Viorica Sofronie-Stokkermans, "Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata", in AVACS Technical Report, (2015), Vol. 111, pp. 52 p.  
    Citation
    Werner Damm, Matthias Horbach, and Viorica Sofronie-Stokkermans, "Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata", in AVACS Technical Report, (2015), Vol. 111, pp. 52 p.
    Export
  • Werner Damm, Matthias Horbach, and Viorica Sofronie-Stokkermans, "Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 186-202.  
    Citation
    Werner Damm, Matthias Horbach, and Viorica Sofronie-Stokkermans, "Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 186-202.
    Export
  • Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, and Andreas Weber, "Detection of Hopf Bifurcations in Chemical Reaction Networks Using Convex Coordinates," Journal of Computational Physics 291, 279-302 (2015).  
    Citation
    Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, and Andreas Weber, "Detection of Hopf Bifurcations in Chemical Reaction Networks Using Convex Coordinates," Journal of Computational Physics 291, 279-302 (2015).
    Export
  • Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, and Andreas Weber, "Detection of Hopf bifurcations in chemical reaction networks using convex coordinates," Journal of Computational Physics 291, 279-302 (2015).  
    Citation
    Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, and Andreas Weber, "Detection of Hopf bifurcations in chemical reaction networks using convex coordinates," Journal of Computational Physics 291, 279-302 (2015).
    Abstract
    We present ecient algorithmic methods to detect Hopf bifurcation xed points in chemical reaction networks with symbolic rate constants, thereby yielding information about the oscillatory behavior of the networks. Our methods use the representations of the systems on convex coordinates that arise from stoichiometric network analysis. One of our methods then reduces the problem of determining the existence of Hopf bifurcation xed points to a rst-order formula over the ordered eld of the reals that can be solved using computational logic packages. The second method uses ideas from tropical geometry to formulate a more ecient method that is incomplete in theory but worked very well for the examples that we have attempted; we have shown it to be able to handle systems involving more than 20 species.
    Export
  • Pascal Fontaine, Thomas Sturm, and Uwe Waldmann, "Foreword to the Special Focus on Constraints and Combinations," Mathematics in Computer Science 9 (3), 265-265 (2015).  
    Citation
    Pascal Fontaine, Thomas Sturm, and Uwe Waldmann, "Foreword to the Special Focus on Constraints and Combinations," Mathematics in Computer Science 9 (3), 265-265 (2015).
    Export
  • Willem Hagemann, Symbolic Orthogonal Projections: A New Polyhedral Representation for Reachability Analysis of Hybrid Systems, PhD Thesis, Universität des Saarlandes, 2015.  
    Citation
    Willem Hagemann, Symbolic Orthogonal Projections: A New Polyhedral Representation for Reachability Analysis of Hybrid Systems, PhD Thesis, Universität des Saarlandes, 2015.
    Export
  • Laurent Hoeltgen, Markus Mainberger, Sebastian Hoffmann, Joachim Weickert, Ching Hoo Tang, Simon Setzer, Daniel Johannsen, Frank Neumann, and Benjamin Doerr, "Optimising Spatial and Tonal Data for PDE-based Inpainting", (2015), pp. 54 p.  
    Citation
    Laurent Hoeltgen, Markus Mainberger, Sebastian Hoffmann, Joachim Weickert, Ching Hoo Tang, Simon Setzer, Daniel Johannsen, Frank Neumann, and Benjamin Doerr, "Optimising Spatial and Tonal Data for PDE-based Inpainting", (2015), pp. 54 p.
    Abstract
    Some recent methods for lossy signal and image compression store only a few selected pixels and fill in the missing structures by inpainting with a partial differential equation (PDE). Suitable operators include the Laplacian, the biharmonic operator, and edge-enhancing anisotropic diffusion (EED). The quality of such approaches depends substantially on the selection of the data that is kept. Optimising this data in the domain and codomain gives rise to challenging mathematical problems that shall be addressed in our work. In the 1D case, we prove results that provide insights into the difficulty of this problem, and we give evidence that a splitting into spatial and tonal (i.e. function value) optimisation does hardly deteriorate the results. In the 2D setting, we present generic algorithms that achieve a high reconstruction quality even if the specified data is very sparse. To optimise the spatial data, we use a probabilistic sparsification, followed by a nonlocal pixel exchange that avoids getting trapped in bad local optima. After this spatial optimisation we perform a tonal optimisation that modifies the function values in order to reduce the global reconstruction error. For homogeneous diffusion inpainting, this comes down to a least squares problem for which we prove that it has a unique solution. We demonstrate that it can be found efficiently with a gradient descent approach that is accelerated with fast explicit diffusion (FED) cycles. Our framework allows to specify the desired density of the inpainting mask a priori. Moreover, is more generic than other data optimisation approaches for the sparse inpainting problem, since it can also be extended to nonlinear inpainting operators such as EED. This is exploited to achieve reconstructions with state-of-the-art quality. We also give an extensive literature survey on PDE-based image compression methods.
    Export
  • Maximilian Jaroschek, Pablo Federico Dobal, and Pascal Fontaine, "Adapting Real Quantifier Elimination Methods for Conflict Set Computation", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 151-166.  
    Citation
    Maximilian Jaroschek, Pablo Federico Dobal, and Pascal Fontaine, "Adapting Real Quantifier Elimination Methods for Conflict Set Computation", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 151-166.
    Export
  • Christopher Junk, Robert Rößger, Georg Rock, Karsten Theis, Christoph Weidenbach, and Patrick Wischnewski, "Model-Based Variant Management with v.control", in Transdisciplinary Lifecycle Analysis of Systems, edited by Richard Curran, Nel Wognum, Milton Borsato, Josip Stiepandic, and Wim J. C. Verhagen (IOS Press, Amsterdam, 2015), pp. 194-203.  
    Citation
    Christopher Junk, Robert Rößger, Georg Rock, Karsten Theis, Christoph Weidenbach, and Patrick Wischnewski, "Model-Based Variant Management with v.control", in Transdisciplinary Lifecycle Analysis of Systems, edited by Richard Curran, Nel Wognum, Milton Borsato, Josip Stiepandic, and Wim J. C. Verhagen (IOS Press, Amsterdam, 2015), pp. 194-203.
    Export
  • Manuel Kauers, Maximilian Jaroschek, and Frederik Johannson, "Ore Polynomials in Sage", in Computer Algebra and Polynomials, edited by Jaime Gutierrez, Josef Schicho, and Martin Weiman (Springer, Berlin, 2015), pp. 105-125.  
    Citation
    Manuel Kauers, Maximilian Jaroschek, and Frederik Johannson, "Ore Polynomials in Sage", in Computer Algebra and Polynomials, edited by Jaime Gutierrez, Josef Schicho, and Martin Weiman (Springer, Berlin, 2015), pp. 105-125.
    Export
  • Felix Klein and Martin Zimmermann, "How Much Lookahead is Needed to Win Infinite Games?", in Automata, Languages, and Programming, edited by Magnus M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann (Springer, Berlin, 2015), pp. 452-463.  
    Citation
    Felix Klein and Martin Zimmermann, "How Much Lookahead is Needed to Win Infinite Games?", in Automata, Languages, and Programming, edited by Magnus M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann (Springer, Berlin, 2015), pp. 452-463.
    Export
  • Felix Klein and Martin Zimmerman, "What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead", in 24th EACSL Annual Conference on Computer Science Logic, edited by Stephan Kreutzer (Wadern, Schloss Dagstuhl, 2015), pp. 519-533.  
    Citation
    Felix Klein and Martin Zimmerman, "What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead", in 24th EACSL Annual Conference on Computer Science Logic, edited by Stephan Kreutzer (Wadern, Schloss Dagstuhl, 2015), pp. 519-533.
    Export
  • Marek Košta, Thomas Sturm, and Andreas Dolzmann, "Better Answers to Real Questions," Journal of Symbolic Computation 74, 255-275 (2016).  
    Citation
    Marek Košta, Thomas Sturm, and Andreas Dolzmann, "Better Answers to Real Questions," Journal of Symbolic Computation 74, 255-275 (2016).
    Abstract
    We consider existential problems over the reals. Extended quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables. Implementations of extended quantifier elimination via virtual substitution have been successfully applied to various problems in science and engineering. So far, the answers produced by these implementations included infinitesimal and infinite numbers, which are hard to interpret in practice. We introduce here a post-processing procedure to convert, for fixed parameters, all answers into standard real numbers. The relevance of our procedure is demonstrated by application of our implementation to various examples from the literature, where it significantly improves the quality of the results.
    Export
  • Marek Košta, Thomas Sturm, and Andreas Dolzmann, "Better Answers to Real Questions", (2015), pp. 25 p.  
    Citation
    Marek Košta, Thomas Sturm, and Andreas Dolzmann, "Better Answers to Real Questions", (2015), pp. 25 p.
    Abstract
    We consider existential problems over the reals. Extended quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables. Implementations of extended quantifier elimination via virtual substitution have been successfully applied to various problems in science and engineering. So far, the answers produced by these implementations included infinitesimal and infinite numbers, which are hard to interpret in practice. We introduce here a post-processing procedure to convert, for fixed parameters, all answers into standard real numbers. The relevance of our procedure is demonstrated by application of our implementation to various examples from the literature, where it significantly improves the quality of the results.
    Export
  • Marek Košta and Thomas Sturm, "A Generalized Framework for Virtual Substitution", (2015), pp. 17 p.  
    Citation
    Marek Košta and Thomas Sturm, "A Generalized Framework for Virtual Substitution", (2015), pp. 17 p.
    Abstract
    We generalize the framework of virtual substitution for real quantifier elimination to arbitrary but bounded degrees. We make explicit the representation of test points in elimination sets using roots of parametric univariate polynomials described by Thom codes. Our approach follows an early suggestion by Weispfenning, which has never been carried out explicitly. Inspired by virtual substitution for linear formulas, we show how to systematically construct elimination sets containing only test points representing lower bounds.
    Export
  • Manuel Lamotte-Schubert, Automatic Authorization Analysis, PhD Thesis, Universität des Saarlandes, 2015.  
    Citation
    Manuel Lamotte-Schubert, Automatic Authorization Analysis, PhD Thesis, Universität des Saarlandes, 2015.
    Export
  • Andrew Reynolds and Jasmin Christian Blanchette, "A Decision Procedure for (Co)datatypes in SMT Solvers", in Automated Deduction -- CADE-25, edited by Amy P. Felty and Aart Middeldorp (Springer, Berlin, 2015), pp. 197-213.  
    Citation
    Andrew Reynolds and Jasmin Christian Blanchette, "A Decision Procedure for (Co)datatypes in SMT Solvers", in Automated Deduction -- CADE-25, edited by Amy P. Felty and Aart Middeldorp (Springer, Berlin, 2015), pp. 197-213.
    Export
  • Renate A. Schmidt and Uwe Waldmann, "Modal Tableau Systems with Blocking and Congruence Closure", in Automated Reasoning with Analytic Tableaux and Related Methods, edited by Hans de Nivelle (Springer, Berlin, 2015), pp. 38-53.  
    Citation
    Renate A. Schmidt and Uwe Waldmann, "Modal Tableau Systems with Blocking and Congruence Closure", in Automated Reasoning with Analytic Tableaux and Related Methods, edited by Hans de Nivelle (Springer, Berlin, 2015), pp. 38-53.
    Export
  • Renate A. Schmidt and Uwe Waldmann, "Modal Tableau Systems with Blocking and Congruence Closure", in eScholar, (2015), pp. 22 p.  
    Citation
    Renate A. Schmidt and Uwe Waldmann, "Modal Tableau Systems with Blocking and Congruence Closure", in eScholar, (2015), pp. 22 p.
    Export
  • Stephan Seufert, Algorithmic Building Blocks for Relationship Analysis over Large Graphs, PhD Thesis, Universität des Saarlandes, 2015.  
    Citation
    Stephan Seufert, Algorithmic Building Blocks for Relationship Analysis over Large Graphs, PhD Thesis, Universität des Saarlandes, 2015.
    Export
  • Viorica Sofronie-Stokkermans, "Hierarchical Reasoning in Local Theory Extensions and Applications", in SYNASC 2014, (IEEE Computer Society, Los Alamitos, CA, 2015), pp. 34-41.  
    Citation
    Viorica Sofronie-Stokkermans, "Hierarchical Reasoning in Local Theory Extensions and Applications", in SYNASC 2014, (IEEE Computer Society, Los Alamitos, CA, 2015), pp. 34-41.
    Export
  • Thomas Sturm, "Subtropical Real Root Finding", in ISSAC'15, edited by Daniel Robertz (ACM, New York, NY, 2015), pp. 347-354.  
    Citation
    Thomas Sturm, "Subtropical Real Root Finding", in ISSAC'15, edited by Daniel Robertz (ACM, New York, NY, 2015), pp. 347-354.
    Export
  • Thomas Sturm, "Subtropical Real Root Finding", (2015), pp. 18 p.  
    Citation
    Thomas Sturm, "Subtropical Real Root Finding", (2015), pp. 18 p.
    Abstract
    We describe a new incomplete but terminating method for real root finding for large multivariate polynomials. We take an abstract view of the polynomial as the set of exponent vectors associated with sign information on the coefficients. Then we employ linear programming to heuristically find roots. There is a specialized variant for roots with exclusively positive coordinates, which is of considerable interest for applications in chemistry and systems biology. An implementation of our method combining the computer algebra system Reduce with the linear programming solver Gurobi has been successfully applied to input data originating from established mathematical models used in these areas. We have solved several hundred problems with up to more than 800000 monomials in up to 10 variables with degrees up to 12. Our method has failed due to its incompleteness in less than 8 percent of the cases.
    Export
  • Martin Suda, "Variable and Clause Elimination for LTL Satisfiability Checking," Mathematics in Computer Science 9 (3), 327-344 (2015).  
    Citation
    Martin Suda, "Variable and Clause Elimination for LTL Satisfiability Checking," Mathematics in Computer Science 9 (3), 327-344 (2015).
    Export
  • Martin Suda, Resolution-based Methods for Linear Temporal Reasoning, PhD Thesis, Universität des Saarlandes, 2015.  
    Citation
    Martin Suda, Resolution-based Methods for Linear Temporal Reasoning, PhD Thesis, Universität des Saarlandes, 2015.
    Export
  • Andreas Teucke and Christoph Weidenbach, "First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation", (2015), pp. 16 p.  
    Citation
    Andreas Teucke and Christoph Weidenbach, "First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation", (2015), pp. 16 p.
    Abstract
    Counterexample-guided abstraction refinement is a well-established technique in verification. In this paper we instantiate the idea for first-order logic theorem proving. Given a clause set $N$ we propose its abstraction into a clause set $N'$ belonging to a decidable first-order fragment. The abstraction preserves satisfiability: if $N'$ is satisfiable, so is $N$. A refutation in $N'$ can then either be lifted to a refutation in $N$, or it guides a refinement of $N$ and its abstraction $N'$ excluding the previously found refutation that is not liftable.
    Export
  • Andreas Teucke and Christoph Weidenbach, "First-order Logic Theorem Proving and Model Building via Approximation and Instantiation", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 85-100.  
    Citation
    Andreas Teucke and Christoph Weidenbach, "First-order Logic Theorem Proving and Model Building via Approximation and Instantiation", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 85-100.
    Export
  • Marco Voigt and Christoph Weidenbach, "Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete", (2015), pp. 25 p.  
    Citation
    Marco Voigt and Christoph Weidenbach, "Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete", (2015), pp. 25 p.
    Abstract
    Linear arithmetic extended with free predicate symbols is undecidable, in general. We show that the restriction of linear arithmetic inequations to simple bounds extended with the Bernays-Sch\"onfinkel-Ramsey free first-order fragment is decidable and NEXPTIME-complete. The result is almost tight because the Bernays-Sch\"onfinkel-Ramsey fragment is undecidable in combination with linear difference inequations, simple additive inequations, quotient inequations and multiplicative inequations.
    Export
  • Christoph Weidenbach, "Automated Reasoning Building Blocks", in Correct System Design, edited by Roland Meyer and André Platzer (Springer, Berlin, 2015), pp. 172-188.  
    Citation
    Christoph Weidenbach, "Automated Reasoning Building Blocks", in Correct System Design, edited by Roland Meyer and André Platzer (Springer, Berlin, 2015), pp. 172-188.
    Export