Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT
- 20 September 2002
- book chapter
- Published by Springer Nature
- p. 236-249
- https://doi.org/10.1007/3-540-45657-0_18
Abstract
No abstract availableKeywords
This publication has 9 references indexed in Scilit:
- Deconstructing ShostakPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- CVC: A Cooperating Validity CheckerPublished by Springer Nature ,2002
- Lazy Theorem Proving for Bounded Model Checking over Infinite DomainsPublished by Springer Nature ,2002
- ChaffPublished by Association for Computing Machinery (ACM) ,2001
- Exploiting Positive Equality in a Logic of Equality with Uninterpreted FunctionsPublished by Springer Nature ,1999
- Deciding Equality Formulas by Small Domains InstantiationsPublished by Springer Nature ,1999
- Validity checking for combinations of theories with equalityPublished by Springer Nature ,1996
- Test pattern generation using Boolean satisfiabilityIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1992
- Simplification by Cooperating Decision ProceduresACM Transactions on Programming Languages and Systems, 1979