Logic programming, that is Horn Clause Logic equipped with a resolution mechanism, provides an expressive framework for first order proving with computational advantages over alternative approaches. Traditionally, resolution mechanisms employ full unification. Recently, however, attention was given to type-theoretic interpretation of logic programming with the focus on universal fragment of Horn Clause Logic where a restricted form of unification suffices—term matching.

It is well-know that resolution steps that proceed by term matching correspond to theorem proving whereas resolution steps that proceed by unification correspond to problem solving. In my talk I elaborate on the idea and present a calculus in style of logic programming that separates unification and matching steps. The distinctive feature of the calculus is that a successful proof by resolution is captured by an explicit proof term.

I show type-theoretic interpretation of the calculus in first-order dependent type theory. The interpretation gives rise to an approach to refinement in first order dependent type theory that translates a refinement problem into a goal and a program in the calculus. The program computes an answer substitution and a proof term. These in turn provide a solution to the refinement problem.