Dependent type theories [ML72] have a long history of being used for theorem proving. One
aspect of type theory which makes it very powerful as a proof language is that it mixes …

Unification is a fundamental process upon which many methods for automated deduction
are based. Unification theory abstracts from the specific applications of this process: it …

It has been argued elsewhere that a logic programming language with function variables
and λ-abstractions within terms makes a good meta-programming language, especially …

Anti-unification (AU) is a fundamental operation for generalization computation used for
inductive inference. It is the dual operation to unification, an operation at the foundation of …

General mathematical reasoning is computationally undecidable, but humans routinely
solve new problems. Moreover, discoveries developed over centuries are taught to …

One of the major challenges of building software systems is to ensure that the various
components fit together in a well-defined manner. This problem is exacerbated by the recent …

A large variety of computing systems, such as compilers, interpreters, static analyzers, and
theorem provers, need to manipulate syntactic objects like programs, types, formulas, and …

Logical frameworks. Page 131 CHAPTER 17 Logical Frameworks Frank Pfenning SECOND
READERS: Robert Harper, Don Sannella, and Jan Smith. Contents 1 Introduction 2 Abstract …

The complete development of a unification algorithm for so-called higher-order patterns, a
subclass of lambda-terms, is presented. The starting point is a formulation of unification by …

We present the spine calculus S→⊸ &⊤ as an efficient representation for the linear λ-
calculus λ→⊸ &⊤ which includes unrestricted functions (→) linear functions (⊸) additive …