2013/08/27 by José Espírito Santo, Ralph Matthes, Luís Pinto
Computer Science · #Algebra over a field #Calculus (dental) #Coinduction #Finitary #Fixed point #Formal proof #Interpretation (philosophy) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematical proof #Representation (politics) #Semantic Web and Ontologies #cs.LO
paper · pdf · doi:10.4204/eptcs.126.3
published as EPTCS 126, 2013, pp. 28-43 · In Proceedings FICS 2013, arXiv:1308.5896
openalex publication_date 2013/08/27 · arxiv created 2013/09/04 · arxiv updated 2013/09/05 · openalex created_date 2016/06/24 · openalex updated_date 2026/08/05
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"ohm 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.