Please use this identifier to cite or link to this item:

Full metadata record
DC FieldValueLanguage
dc.contributor.authorPinto, Luís F.-
dc.contributor.authorDyckhoff, Roy-
dc.identifier.citationCOOPER, S. Barry ; TRUSS, John K., ed. - “Sets and proofs : invited papers from Logic Colloquium ’97, European Meeting of the Association for Symbolic Logic, Leeds, July 1997”. Cambridge : Cambridge University Press, 1999. ISBN 0-521-63549-7. p. 53-65.eng
dc.description.abstractWe 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.eng
dc.description.sponsorshipCentro de Matemática da Universidade do Minho (CMAT).eng
dc.description.sponsorshipUnião Europeia (UE) - Programa ESPRIT - BRA 7232 Gentzen.eng
dc.publisherCambridge University Presseng
dc.subjectProof seacheng
dc.subjectConstructive logiceng
dc.subjectSequent calculuseng
dc.titleProof search in constructive logicseng
Appears in Collections:CMAT - Artigos em atas de conferências e capítulos de livros com arbitragem / Papers in proceedings of conferences and book chapters with peer review

Files in This Item:
File Description SizeFormat 
ASL97.pdf176,75 kBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID