Proof Generation in the Touchstone Theorem Prover
- 1 January 2000
- book chapter
- Published by Springer Nature
Abstract
No abstract availableKeywords
This publication has 15 references indexed in Scilit:
- Proof-carrying codePublished by Association for Computing Machinery (ACM) ,1997
- Combining decision procedures in the HOL systemPublished by Springer Nature ,1995
- A framework for defining logicsJournal of the ACM, 1993
- A Lazy Approach to Fully-Expansive Theorem ProvingPublished by Elsevier ,1993
- Uniform proofs as a foundation for logic programmingAnnals of Pure and Applied Logic, 1991
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple UnificationJournal of Logic and Computation, 1991
- A Polynomial Time Algorithm for Solving Systems of Linear Inequalities with Two Variables Per InequalitySIAM Journal on Computing, 1980
- Variations on the Common Subexpression ProblemJournal of the ACM, 1980
- Fast Decision Procedures Based on Congruence ClosureJournal of the ACM, 1980
- Simplification by Cooperating Decision ProceduresACM Transactions on Programming Languages and Systems, 1979