Model Evolution with Equality Modulo Built-in Theories
From MaRDI portal
Publication:5200017
DOI10.1007/978-3-642-22438-6_9zbMath1341.68180OpenAlexW29327042MaRDI QIDQ5200017
Peter Baumgartner, Cesare Tinelli
Publication date: 29 July 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_9
Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items (3)
Axiomatic Constraint Systems for Proof Search Modulo Theories ⋮ Structured learning modulo theories ⋮ The Relative Power of Semantics and Unification
Cites Work
- Refutational theorem proving for hierarchic first-order theories
- Solving SAT and SAT Modulo Theories
- Integrating Linear Arithmetic into Superposition Calculus
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Superposition Modulo Linear Arithmetic SUP(LA)
- Superposition and Model Evolution Combined
- Theory Instantiation
- Automated Deduction – CADE-20
- (LIA) - Model Evolution with Linear Integer Arithmetic Constraints
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
This page was built for publication: Model Evolution with Equality Modulo Built-in Theories
