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 Stålmarck’s method.
Semantics and proof-theory of depth-bounded Boolean logics / M. D'Agostino, M. Finger, D.M. Gabbay. - In: THEORETICAL COMPUTER SCIENCE. - ISSN 0304-3975. - 480(2013 Apr), pp. 43-68.
|Titolo:||Semantics and proof-theory of depth-bounded Boolean logics|
D'AGOSTINO, MARCELLO (Corresponding)
|Parole Chiave:||Boolean logic; tractability; natural deduction; automated deduction|
|Settore Scientifico Disciplinare:||Settore M-FIL/02 - Logica e Filosofia della Scienza|
Settore INF/01 - Informatica
Settore MAT/01 - Logica Matematica
|Data di pubblicazione:||apr-2013|
|Digital Object Identifier (DOI):||http://dx.doi.org/10.1016/j.tcs.2013.02.014|
|Appare nelle tipologie:||01 - Articolo su periodico|