A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
From MaRDI portal
Publication:5505560
DOI10.1007/978-3-540-89439-1_20zbMath1182.03035OpenAlexW1810306334MaRDI QIDQ5505560
Publication date: 27 January 2009
Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-89439-1_20
Related Items
Beagle – A Hierarchic Superposition Theorem Prover, Theorem Proving with Bounded Rigid E-Unification, Efficient Algorithms for Bounded Rigid E-unification, Integrating Simplex with Tableaux, Proof generalization in \(\mathrm {LK}\) by second order unifier minimization, The 11th IJCAR automated theorem proving system competition – CASC-J11, Solving constrained Horn clauses over algebraic data types, Free Variables and Theories: Revisiting Rigid E-unification, Axiomatic Constraint Systems for Proof Search Modulo Theories, Superposition as a decision procedure for timed automata, An interpolating sequent calculus for quantifier-free Presburger arithmetic, First-order automated reasoning with theories: when deduction modulo theory meets practice, Unnamed Item, Unnamed Item, Making theory reasoning simpler, Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories, Structured learning modulo theories, Ranking function synthesis for bit-vector relations, Linear Quantifier Elimination as an Abstract Decision Procedure, An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic, Model Evolution with Equality Modulo Built-in Theories, Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic, GRUNGE: a grand unified ATP challenge, Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic, Reasoning in the theory of heap: satisfiability and interpolation
Uses Software
