Semantics and proof-theory of depth bounded Boolean logics

Author(s)

D'Agostino, Marcello ^[1] ; Finger, Marcelo ^[2] ; Gabbay, Dov ^{[3, 4, 5]}

Affiliation

^[1] Univ Ferrara, Dept Econ & Management, I-44100 Ferrara - Italy

^[2] Univ Sao Paulo, Dept Comp Sci, BR-05508 Sao Paulo - Brazil

^[3] Kings Coll London, London WC2R 2LS - England

^[4] Bar Ilan Univ, IL-52100 Ramat Gan - Israel

^[5] Univ Luxembourg, Luxembourg - Luxembourg

• Document type: Journal article
• Source: THEORETICAL COMPUTER SCIENCE; v. 480, p. 43-68, APR 8 2013.
• Web of Science Citations: 7

Abstract

We present a unifying semantical and proof-theoretical framework for investigating depth-bounded approximations to Boolean Logic, namely approximations in which the number of nested applications of a single structural rule, representing the classical Principle of Bivalence, is bounded above by a fixed natural number. These approximations provide a hierarchy of tractable logical systems that indefinitely converge to classical propositional logic. The framework we present here brings to light a general approach to logical inference that is quite different from the standard Gentzen-style approaches, while preserving some of their nice proof-theoretical properties, and is common to several proof systems and algorithms, such as KE, KI and Stalmarck's method. (C) 2013 Elsevier B.V. All rights reserved. (AU)

• FAPESP's process: 08/03995-5 - Logprob: probabilistic logic --- foundations and computational applications
• Grantee: Marcelo Finger
• Support Opportunities: Research Projects - Thematic Grants
• FAPESP's process: 10/51038-0 - Logical consequence, reasoning and computation - LOGCONS
• Grantee: Walter Alexandre Carnielli
• Support Opportunities: Research Projects - Thematic Grants
• FAPESP's process: 11/19860-4 - Deductive-probabilistic reasoning: algorithms and applications
• Grantee: Marcelo Finger
• Support Opportunities: Scholarships abroad - Research