Theorem Proving Using Lazy Proof Explication
- 1 January 2003
- book chapter
- Published by Springer Nature
Abstract
No abstract availableKeywords
This publication has 16 references indexed in Scilit:
- Modeling and Verification of Out-of-Order Microprocessors in UCLIDPublished by Springer Nature ,2002
- Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted FunctionsPublished by Springer Nature ,2002
- Checking Satisfiability of First-Order Formulas by Incremental Translation to SATPublished by Springer Nature ,2002
- A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical PropositionsPublished by Springer Nature ,2002
- ChaffPublished by Association for Computing Machinery (ACM) ,2001
- Boolean Satisfiability with Transitivity ConstraintsPublished by Springer Nature ,2000
- Proof Generation in the Touchstone Theorem ProverPublished by Springer Nature ,2000
- Exploiting Positive Equality in a Logic of Equality with Uninterpreted FunctionsPublished by Springer Nature ,1999
- Validity checking for combinations of theories with equalityPublished by Springer Nature ,1996
- A Computing Procedure for Quantification TheoryJournal of the ACM, 1960