Lecture Notes in Computer Science, 2000, Volume 1861/2000, 254-268, DOI: 10.1007/3-540-44957-4_17

Goal-Directed Proof Search in Multiple-Conclusioned Intuitionistic Logic

James Harland, Tatjana Lutovac and Michael Winikoff

View Related Documents

Abstract

A key property in the definition of logic programming languages is the completeness of goal-directed proofs. This concept originated in the study of logic programming languages for intuitionistic logic in the (single-conclusioned) sequent calculus LJ, but has subsequently been adapted to multiple-conclusioned systems such as those for linear logic. Given these developments, it seems interesting to investigate the notion of goal-directed proofs for a multiple-conclusioned sequent calculus for intuitionistic logic, in that this is a logic for which there are both single-conclusioned and multiple-conclusioned systems (although the latter are less well known). In this paper we show that the language obtained for the multiple-conclusioned system differs from that for the single-conclusioned case, show how hereditary Harrop formulae can be recovered, and investigate contraction-free fragments of the logic.

Fulltext Preview

Image of the first page of the fulltext document