Combining decision procedures in the HOL system
- 1 January 1995
- book chapter
- Published by Springer Nature in Lecture Notes in Computer Science
Abstract
No abstract availableKeywords
This publication has 9 references indexed in Scilit:
- Lazy techniques for fully expansive theorem provingFormal Methods in System Design, 1993
- EVES: An overviewLecture Notes in Computer Science, 1991
- Deciding Combinations of TheoriesJournal of the ACM, 1984
- Reasoning About Recursively Defined Data StructuresJournal 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
- A Practical Decision Procedure for Arithmetic with Function SymbolsJournal of the ACM, 1979
- An algorithm for reasoning about equalityCommunications of the ACM, 1978
- On the SUP-INF Method for Proving Presburger FormulasJournal of the ACM, 1977