Proof Search in Constructive Logics

Summary

Abstract

We present an overview of some sequent calculi organised not for “theorem-proving” but for proof search, where the proofs themselves (and the avoidance of known proofs on backtracking) are objects of interest. The main calculus discussed is that of Herbelin [1994] for intuitionistic logic, which extends methods used in hereditary Harrop logic programming; we give a brief discussion of some similar calculi for other logics. We also point to some related work on permutations in intuitionistic Gentzen sequent calculi that clarifies the relationship between such calculi and natural deduction.

Introduction

It is widely held that ordinary logic programming is based on classical logic, with a Tarski-style semantics (answering questions “What judgments are provable?”) rather than a Heyting-style semantics (answering questions like “What are the proofs, if any, of each judgment?”). If one adopts the latter style (equivalently, the BHK interpretation: see [35] for details) by regarding proofs as answers to questions, or as solutions to problems, then proof-enumeration rather than theorem-proving is the issue. See [12] for discussion of differences between the two styles of semantics.

Some authors (e.g. [25]) have shown that as an adequate basis for pure Prolog one can, instead of classical logic, take the Horn fragment of minimal logic, and that this can be extended up to the hereditary Harrop fragment of minimal (or, equivalently, intuitionistic) logic, thus providing [24] a good logical basis for software engineering features such as scoping and modularity. In such work, the emphasis is on provability: the semantics is Tarski-style rather than Heyting-style.