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 |
