A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
From MaRDI portal
Publication:5505560
DOI10.1007/978-3-540-89439-1_20zbMATH Open1182.03035OpenAlexW1810306334MaRDI QIDQ5505560FDOQ5505560
Authors: Philipp Rümmer 
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
Recommendations
- scientific article; zbMATH DE number 218517
- scientific article; zbMATH DE number 2152687
- Sequent Calculi for Intuitionistic Linear Logic with Strong Negation
- scientific article; zbMATH DE number 1538011
- A sequent calculus for first-order logic formalized in Isabelle/HOL
- A Linear-Logic Semantics for Constraint Handling Rules
- Formalized meta-theory of sequent calculi for linear logics
- Tools and Algorithms for the Construction and Analysis of Systems
- A first-order sequent calculus for logical inferentialists and expressivists
- Extended Lambek calculi and first-order linear logic
Cited In (34)
- Title not available (Why is that?)
- Reasoning in the theory of heap: satisfiability and interpolation
- Theorem proving with bounded rigid \(E\)-unification
- A constant-space sequential model of computation for first-order logic
- Free variables and theories: revisiting rigid \(E\)-unification
- Axiomatic constraint systems for proof search modulo theories
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Title not available (Why is that?)
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
- Solving constrained Horn clauses over algebraic data types
- (LIA) - Model Evolution with Linear Integer Arithmetic Constraints
- GRUNGE: a grand unified ATP challenge
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
- Beyond quantifier-free interpolation in extensions of Presburger arithmetic
- Ranking function synthesis for bit-vector relations
- Making theory reasoning simpler
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
- A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
- Superposition as a decision procedure for timed automata
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- Model Evolution with Equality Modulo Built-in Theories
- Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
- The 11th IJCAR automated theorem proving system competition – CASC-J11
- Structured learning modulo theories
- Linear quantifier elimination as an abstract decision procedure
- ALASCA: reasoning in quantified linear arithmetic
- Decision procedures for sequence theories
- Range-restricted and Horn interpolation through clausal tableaux
- Beagle -- a hierarchic superposition theorem prover
- Efficient algorithms for bounded rigid \(E\)-unification
- Integrating Linear Arithmetic into Superposition Calculus
- Integrating simplex with tableaux
Uses Software
This page was built for publication: A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5505560)
