SMELS: Satisfiability Modulo Equality with Lazy Superposition

DOI10.1007/978-3-540-88387-6_15zbMath1183.68559OpenAlexW1860739477MaRDI QIDQ3540073

No author found.

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

Related Items

Combining Instance Generation and Resolution, Theory decision by decomposition

Uses Software

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

Cites Work

• A rewriting approach to satisfiability procedures.
• The model evolution calculus as a first-order DPLL method
• Simplify: a theorem prover for program checking
• Integrating Linear Arithmetic into Superposition Calculus
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item