A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
From MaRDI portal
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
(38)- A constant-space sequential model of computation for first-order logic
- 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
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
- Beagle -- a hierarchic superposition theorem prover
- Theorem proving with bounded rigid E-unification
- Efficient algorithms for bounded rigid E-unification
- Integrating simplex with tableaux
- Integrating Linear Arithmetic into Superposition Calculus
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- scientific article; zbMATH DE number 7453201 (Why is no real title available?)
- Structured learning modulo theories
- Model Evolution with Equality Modulo Built-in Theories
- (LIA) - Model Evolution with Linear Integer Arithmetic Constraints
- 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
- scientific article; zbMATH DE number 7806143 (Why is no real title available?)
- A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
- Symbolic Model Construction for Saturated Constrained Horn Clauses
- ALASCA: reasoning in quantified linear arithmetic
- Decision procedures for sequence theories
- Range-restricted and Horn interpolation through clausal tableaux
- Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
- On solving string equations via powers and Parikh images
- Cooking string-integer conversions with noodles
- CHC-COMP 2023: competition report
- An empirical assessment of progress in automated theorem proving
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)
