Pages that link to "Item:Q5505560"
From MaRDI portal
The following pages link to A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic (Q5505560):
Displaying 26 items.
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization (Q331619) (← links)
- An interpolating sequent calculus for quantifier-free Presburger arithmetic (Q438556) (← links)
- Structured learning modulo theories (Q511777) (← links)
- Superposition as a decision procedure for timed automata (Q1949086) (← links)
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic (Q2058375) (← links)
- Reasoning in the theory of heap: satisfiability and interpolation (Q2119112) (← links)
- First-order automated reasoning with theories: when deduction modulo theory meets practice (Q2209546) (← links)
- Making theory reasoning simpler (Q2233504) (← links)
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories (Q2234101) (← links)
- Ranking function synthesis for bit-vector relations (Q2248069) (← links)
- GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
- Free Variables and Theories: Revisiting Rigid E-unification (Q2964448) (← links)
- Axiomatic Constraint Systems for Proof Search Modulo Theories (Q2964465) (← links)
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Q3075472) (← links)
- Beagle – A Hierarchic Superposition Theorem Prover (Q3454107) (← links)
- Theorem Proving with Bounded Rigid E-Unification (Q3454123) (← links)
- Efficient Algorithms for Bounded Rigid E-unification (Q3455762) (← links)
- Integrating Simplex with Tableaux (Q3455763) (← links)
- (Q5020662) (← links)
- Model Evolution with Equality Modulo Built-in Theories (Q5200017) (← links)
- Linear Quantifier Elimination as an Abstract Decision Procedure (Q5747770) (← links)
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic (Q5747778) (← links)
- The 11th IJCAR automated theorem proving system competition – CASC-J11 (Q6095787) (← links)
- Decision procedures for sequence theories (Q6535526) (← links)
- Range-restricted and Horn interpolation through clausal tableaux (Q6541142) (← links)
- Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification (Q6661749) (← links)
