SMELS: Satisfiability Modulo Equality with Lazy Superposition

DOI10.1007/978-3-540-88387-6_15MaRDI QIDQ3540073zbMATH OpenOpenAlexFDO

Authors

Publication date 20 November 2008

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-88387-6_15

Mathematics Subject Classification ID

Recommendations

• SMELS: satisfiability modulo equality with lazy superposition
• Superposition with equivalence reasoning and delayed clause normal form transformation.
• Engineering DPLL(T) + Saturation
• Superposition with equivalence reasoning and delayed clause normal form transformation
• Theoretical Aspects of Computing – ICTAC 2005

Cites work

• A rewriting approach to satisfiability procedures.
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 1348470 (Why is no real title available?)
• Integrating Linear Arithmetic into Superposition Calculus
• Paramodulation-based theorem proving
• Resolution theorem proving
• Simplify: a theorem prover for program checking
• The model evolution calculus as a first-order DPLL method

Cited in

(6)

• Theory decision by decomposition
• Unification with abstraction and theory instantiation in saturation-based reasoning
• SMELS: satisfiability modulo equality with lazy superposition
• Computing All Implied Equalities via SMT-Based Partition Refinement
• Congruence closure with free variables
• Combining instance generation and resolution

Describes a project that uses

Uses Software

• VAMPIRE
• SPASS
• Yices
• cvc3
• z3
• SIMPLIFY
• E Theorem Prover

This page was built for publication: SMELS: Satisfiability Modulo Equality with Lazy Superposition

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3540073)