Specifying and implementing theorem provers in a higher-order logic programming language
Amy Felty, Dale Armin Miller · 1989
We argue that a logic programming language with a higher-order intuitionistic logic as its foundation can be used both to naturally specify and implement theorem provers. The language extends traditional logic programming languages by replacing first-order terms with simply-typed λ-terms, replacing first-order unification with higher-order unification, and allowing implication and universal quantification in queries and the bodies of clauses. Inference rules for a variety of proof systems can be naturally specified in this language. The higher-order features of the language contribute to a concise specification of provisos concerning variable occurrences in formulas and the discharge of assumptions present in many proof systems. In addition, abstraction in meta-terms allows the construction of terms representing object level proofs which capture the notions of abstractions found in many proof systems. The operational interpretations of the connectives of the language provide a set of basic search operations which describe goal-directed search for proofs. To emphasize the generality of the meta-language, we compare it to another general specification language: the Logical Framework (LF). We describe a translation which compiles a specification of a logic in LF to a set of formulas of our meta-language, and