(University of Dundee)

In constructive proof theory, proving that a proposition A has a proof in the context Gamma amounts to showing that type A is inhabited by a proof p in the context Gamma, namely it amounts to constructing p. This principle underlies most modern interactive theorem provers, e.g. Coq or Agda.First-order automated theorem proving, in contrast, has much weaker, if any, support for capturing structural (constructive) properties of proofs. To prove that a proposition A follows from a logic program Gamma, the algorithm of SLD-resolution should derive a contradiction from assumption that A is false. The proof structure remains irrelevant in this decision procedure, as long as resolution algorithm succeeds in finding a contradiction.

The resolution approach has advantages, the main of which is efficient proof automation. However, neglecting proof structure comes at a price. It is extremely hard to analyse structural properties of programs. One striking example is the fact that in 40 years since introduction of logic programming, the community has never reached a consensus on the notion of universal termination of logic programs, let alone semi-deciding that property. In contrast, universal termination of Coq programs can be semi-decided by imposing the structural recursion check. In logic programming we can only talk about termination of individual SLD-derivations, for goals of certain kinds, so we can only work with various forms of existential termination.

In this talk, I will show how the recent coalgebraic semantics of logic programming inspired a new structural approach to untyped theorem proving. Structural automated proving is the analogue of constructive approach but realised in the untyped first-order setting. In particular, it allows to formulate a new general theory of universal productivity and coinduction in logic programming for the first time.

Video Conferencing Room

Department of Computer Science