OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

A Coinductive Approach to Proof Search

Espírito Santo, José and Matthes, Ralph and Pinto, Luís A Coinductive Approach to Proof Search. (2013) In: Fixed Points in Computer Science (FICS 2013), 1 September 2013 (Turin, Italy).

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
388kB

Official URL: http://dx.doi.org/10.4204/EPTCS.126.3

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). <p> 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.

Item Type:Conference or Workshop Item (Paper)
HAL Id:hal-01226485
Audience (conference):National conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > Universidade do Minho (PORTUGAL)
Laboratory name:
Statistics:download
Deposited By: IRIT IRIT
Deposited On:16 Oct 2015 09:24

Repository Staff Only: item control page