A proof procedure for the logic of hereditary Harrop formulas
- 1 January 1993
- journal article
- Published by Springer Nature in Journal of Automated Reasoning
- Vol. 11 (1) , 115-145
- https://doi.org/10.1007/bf00881902
Abstract
No abstract availableThis publication has 14 references indexed in Scilit:
- Specifying theorem provers in a higher-order logic programming languagePublished by Springer Nature ,2005
- Unification under a mixed prefixJournal of Symbolic Computation, 1992
- 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
- Higher-order Horn clausesJournal of the ACM, 1990
- First-Order Logic and Automated Theorem ProvingPublished by Springer Nature ,1990
- Clausal intuitionistic logic II. tableau proof proceduresThe Journal of Logic Programming, 1988
- An Efficient Unification AlgorithmACM Transactions on Programming Languages and Systems, 1982
- The Semantics of Predicate Logic as a Programming LanguageJournal of the ACM, 1976
- A unification algorithm for typed