Focussing and Proof construction
This paper proposes a synthetic presentation of the Proof Construction paradigm, which underlies most of the
research and development in the so-called "logic programming" area. Two essential aspects of this paradigm
are discussed here: true non-determinism et partial information. A new formulation of Focussing, the basic
property used to deal with non-determinism in proof construction, is presented. This formulation is then used
to introduce a general constraint-based technique capable of dealing with partial information in proof
construction. One of the baselines of the paper is to avoid to rely on syntax to describe the key mechanisms
of the paradigm. In fact, the bipolar decomposition of formulas captures their main structure, which can then
be directly mapped into a sequent system that uses only atoms. This system thus completely "dissolves" the
syntax of the formulas and retains only their behavioural content as far as proof construction is concerned.
One step further is taken with so called "abstract" proofs, which dissolves in a similar way the specific tree-like
syntax of the proofs themselves and retains only what is relevant to proof construction.
Annals of Pure and Applied Logic, 107(1), pp 131-163, Elsevier
paper.pdf (179.85 kB)
paper.ps (238.00 kB)