Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/3819
Título: | Cut formulae and logic programming |
Autor(es): | Pinto, Luís F. |
Palavras-chave: | Proof search Sequent calculus Cut-rule Logic programming |
Data: | 1994 |
Editora: | Springer Verlag |
Citação: | DYCKHOFF, Roy, ed. – “Extensions of logic programming : 4th International Workshop, ELP '93, St Andrews, U.K., March 29 - April 1, 1993. Proceedings”. Berlin : Springer-Verlag, cop. 1994. ISBN: 3-540-58025-5. p. 282-300. |
Resumo(s): | In this paper we present a mechanism to define names for proof-witnesses of formulae and thus to use Gentzen's cut-rule in logic programming. We consider a program to be a set of logical formulae together with a list of such definitions. Occurrences of the defined names guide the proof-search by indicating when an instance of the cut-rule should be attempted. By using the cut-rule there are proofs that can be made dramatically shorter. We explain how this idea of using the cut-rule can be applied to the logic of hereditary Harrop formulae. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/3819 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
cut.ps | 196,17 kB | Postscript | Ver/Abrir | |
cut.pdf | 229,21 kB | Adobe PDF | Ver/Abrir |