Amy Felty and Dale Miller. In

**Abstract:**
Since logic programming systems directly implement search and
unification and since these operations are essential for the
implementation of most theorem provers, logic programming languages
should make ideal implementation languages for theorem provers. We
shall argue that this is indeed the case if the logic programming
language is extended in several ways. We present an extended logic
programming language where first-order terms are replaced with
simply-typed lambda-terms, higher-order unification replaces
first-order unification, and implication and universal quantification
are allowed in queries and the bodies of clauses. This language
naturally specifies inference rules for various proof systems. The
primitive search operations required to search for proofs generally
have very simple implementations using the logical connectives of this
extended logic programming language. Higher-order unification, which
provides sophisticated pattern matching on formulas and proofs, can be
used to determine when and at what instance an inference rule can be
employed in the search for a proof. Tactics and tacticals, which
provide a framework for high-level control over search, can also be
directly implemented in this extended language. The theorem provers
presented in this paper have been implemented in the higher-order
logic programming language lambda-Prolog.