Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/25226
Título: | A coinductive approach to proof search |
Autor(es): | Espírito Santo, José Matthes, Ralph Pinto, Luís F. |
Palavras-chave: | Proof search Coinduction Intuitionistic logic Lambda-calculus |
Data: | 28-Ago-2013 |
Editora: | Open Publishing Association |
Revista: | Electronic Proceedings in Theoretical Computer Science (EPTCS) |
Resumo(s): | We propose to study proof search from a coinductive point of view. In this paper, we consider intuitionistic logic and a focused system based on Herbelin’s LJT for the implicational fragment. We introduce a variant of lambda calculus with potentially infinitely deep terms and a means of expressing alternatives for the description of the “solution spaces” (called Böhm forests), which are a representation of all (not necessarily well-founded but still locally well-formed) proofs of a given formula (more generally: of a given sequent). As main result we obtain, for each given formula, the reduction of a coinductive definition of the solution space to a effective coinductive description in a finitary term calculus with a formal greatest fixed-point operator. This reduction works in a quite direct manner for the case of Horn formulas. For the general case, the naive extension would not even be true. We need to study “co-contraction” of contexts (contraction bottom-up) for dealing with the varying contexts needed beyond the Horn fragment, and we point out the appropriate finitary calculus, where fixed-point variables are typed with sequents. Co-contraction enters the interpretation of the formal greatest fixed points - curiously in the semantic interpretation of fixed-point variables and not of the fixed-point operator. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/25226 |
DOI: | 10.4204/EPTCS.126.3 |
ISSN: | 2075-2180 |
Versão da editora: | http://rvg.web.cse.unsw.edu.au/eptcs/paper.cgi?FICS13.3 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
CoinductiveProofSearchFICS2013EPTCS.pdf | Documento principal | 256 kB | Adobe PDF | Ver/Abrir |