Proof search in constructive logics

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,...

Full description

Bibliographic Details
Main Author: Pinto, Luís F. (author)
Other Authors: Dyckhoff, Roy (author)
Format: conferencePaper
Language:eng
Published: 1999
Subjects:
Online Access:http://hdl.handle.net/1822/3828
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/3828
Description
Summary: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 similar calculi for other logics. We also point out to some related work on permutations in intuitionistic Gentzen sequent calculi that clarifies the relationship between such calculi and natural deduction.