Embedding complex decision procedures inside an interactive theorem prover
- 1 September 1993
- journal article
- Published by Springer Nature in Annals of Mathematics and Artificial Intelligence
- Vol. 8 (3) , 475-502
- https://doi.org/10.1007/bf01530803
Abstract
No abstract availableKeywords
This publication has 16 references indexed in Scilit:
- Solving propositional satisfiability problemsAnnals of Mathematics and Artificial Intelligence, 1990
- Nonclausal deduction in first-order temporal logicJournal of the ACM, 1990
- Algorithms for testing the satisfiability of propositional formulaeThe Journal of Logic Programming, 1989
- Completely non-clausal theorem provingArtificial Intelligence, 1982
- Theorem Proving via General MatingsJournal of the ACM, 1981
- A Basis for Theoretical Computer SciencePublished by Springer Nature ,1981
- Reasoning About Recursively Defined Data StructuresJournal of the ACM, 1980
- Fast Decision Procedures Based on Congruence ClosureJournal of the ACM, 1980
- The mathematical language AUTOMATH, its usage, and some of its extensionsPublished by Springer Nature ,1970
- A Computing Procedure for Quantification TheoryJournal of the ACM, 1960