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 (25)
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
This page was built for publication: A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
