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.03035MaRDI 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
03B35: Mechanization of proofs and logical operations
Related Items
Unnamed Item, Model Evolution with Equality Modulo Built-in Theories, Linear Quantifier Elimination as an Abstract Decision Procedure, An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic, The 11th IJCAR automated theorem proving system competition – CASC-J11, Solving constrained Horn clauses over algebraic data types, Proof generalization in \(\mathrm {LK}\) by second order unifier minimization, An interpolating sequent calculus for quantifier-free Presburger arithmetic, Structured learning modulo theories, Superposition as a decision procedure for timed automata, Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic, Reasoning in the theory of heap: satisfiability and interpolation, First-order automated reasoning with theories: when deduction modulo theory meets practice, Making theory reasoning simpler, Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories, Ranking function synthesis for bit-vector relations, GRUNGE: a grand unified ATP challenge, Free Variables and Theories: Revisiting Rigid E-unification, Axiomatic Constraint Systems for Proof Search Modulo Theories, Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic, Beagle – A Hierarchic Superposition Theorem Prover, Theorem Proving with Bounded Rigid E-Unification, Efficient Algorithms for Bounded Rigid E-unification, Integrating Simplex with Tableaux
Uses Software
