An interpolating theorem prover
Top Cited Papers
- 21 November 2005
- journal article
- Published by Elsevier in Theoretical Computer Science
- Vol. 345 (1) , 101-121
- https://doi.org/10.1016/j.tcs.2005.07.003
Abstract
No abstract availableKeywords
This publication has 12 references indexed in Scilit:
- Abstractions from proofsPublished by Association for Computing Machinery (ACM) ,2004
- Automatic Abstraction without CounterexamplesPublished by Springer Nature ,2003
- A Symbolic Approach to Predicate AbstractionPublished by Springer Nature ,2003
- Interpolation and SAT-Based Model CheckingPublished by Springer Nature ,2003
- Lazy Theorem Proving for Bounded Model Checking over Infinite DomainsPublished by Springer Nature ,2002
- Lower bounds for resolution and cutting plane proofs and monotone computationsThe Journal of Symbolic Logic, 1997
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmeticThe Journal of Symbolic Logic, 1997
- A Structure-preserving Clause Form TranslationJournal of Symbolic Computation, 1986
- Simplification by Cooperating Decision ProceduresACM Transactions on Programming Languages and Systems, 1979
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theoryThe Journal of Symbolic Logic, 1957