Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT
- 20 September 2002
- book chapter
- Published by Springer Nature in Lecture Notes in Computer Science
- 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 CheckerLecture Notes in Computer Science, 2002
- Lazy Theorem Proving for Bounded Model Checking over Infinite DomainsLecture Notes in Computer Science, 2002
- ChaffPublished by Association for Computing Machinery (ACM) ,2001
- Exploiting Positive Equality in a Logic of Equality with Uninterpreted FunctionsLecture Notes in Computer Science, 1999
- Deciding Equality Formulas by Small Domains InstantiationsLecture Notes in Computer Science, 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