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