Semantics and proof-theory of depth bounded Boolean logics

Autor(es)

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

Afiliação do(s) autor(es)

^[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

• Tipo de documento: Artigo Científico
• Fonte: THEORETICAL COMPUTER SCIENCE; v. 480, p. 43-68, APR 8 2013.
• Citações Web of Science: 8

Resumo

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)

• Processo FAPESP: 11/19860-4 - Raciocínio lógico-probabilístico: algoritmos e aplicações
• Beneficiário: Marcelo Finger
• Linha de fomento: Bolsas no Exterior - Pesquisa
• Processo FAPESP: 10/51038-0 - Logical consequence, reasoning and computation - LOGCONS
• Beneficiário: Walter Alexandre Carnielli
• Linha de fomento: Auxílio à Pesquisa - Temático
• Processo FAPESP: 08/03995-5 - LOGPROB: lógica probabilística - fundamentos e aplicações computacionais
• Beneficiário: Marcelo Finger
• Linha de fomento: Auxílio à Pesquisa - Temático