A Coinductive Approach to Proof SearchReportar como inadecuado




A Coinductive Approach to Proof Search - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 University of Minho Portugal 2 IRIT - Institut de recherche en informatique de Toulouse

Abstract : 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.

Keywords : Logic in computer science





Autor: José Espírito Santo - Ralph Matthes - Luís Pinto -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados