Towards depth-bounded natural deduction for classical first-order logic

Marcello D’agostino; Costanza Larese; Sanjay Modgil

Towards depth-bounded natural deduction for classical first-order logic

Marcello D’agostino, Costanza Larese, Sanjay Modgil

Research output: Contribution to journal › Article › peer-review

3 Citations (Scopus)

Abstract

In this paper we lay the foundations of a new proof-theory for classical first-order logic that allows for a natural characterization of a notion of inferential depth. The approach we propose here aims towards extending the proof-theoretical framework presented in [6] by combining it with some ideas inspired by Hin-tikka’s work [18]. Unlike standard natural deduction, in this framework the inference rules that fix the meaning of the logical operators are symmetrical with respect to assent and dissent and do not involve the discharge of formulas. The only discharge rule is a classical dilemma rule whose nested applications provide a sensible measure of inferential depth. The result is a hierarchy of decidable depth-bounded approximations of classical first-order logic that ex-pands the hierarchy of tractable approximations of Boolean logic investigated in [11, 10, 7].

Original language	English
Pages (from-to)	423-451
Number of pages	29
Journal	IfCoLoG Journal of Logics and their Applications
Volume	8
Issue number	2
Publication status	Published - Mar 2021

Cite this

@article{ddea5925594448ac94baa1d8be605bdf,

title = "Towards depth-bounded natural deduction for classical first-order logic",

abstract = "In this paper we lay the foundations of a new proof-theory for classical first-order logic that allows for a natural characterization of a notion of inferential depth. The approach we propose here aims towards extending the proof-theoretical framework presented in [6] by combining it with some ideas inspired by Hin-tikka{\textquoteright}s work [18]. Unlike standard natural deduction, in this framework the inference rules that fix the meaning of the logical operators are symmetrical with respect to assent and dissent and do not involve the discharge of formulas. The only discharge rule is a classical dilemma rule whose nested applications provide a sensible measure of inferential depth. The result is a hierarchy of decidable depth-bounded approximations of classical first-order logic that ex-pands the hierarchy of tractable approximations of Boolean logic investigated in [11, 10, 7].",

author = "Marcello D{\textquoteright}agostino and Costanza Larese and Sanjay Modgil",

note = "Funding Information: Funded by the Italian Ministry of University (MUR) as part of the the PRIN 2017 project n. 20173YP4N3. Publisher Copyright: {\textcopyright} 2021, College Publications. All rights reserved. Copyright: Copyright 2021 Elsevier B.V., All rights reserved.",

year = "2021",

month = mar,

language = "English",

volume = "8",

pages = "423--451",

journal = "IfCoLoG Journal of Logics and their Applications",

issn = "2631-9810",

publisher = "College Publications",

number = "2",

}

TY - JOUR

T1 - Towards depth-bounded natural deduction for classical first-order logic

AU - D’agostino, Marcello

AU - Larese, Costanza

AU - Modgil, Sanjay

N1 - Funding Information: Funded by the Italian Ministry of University (MUR) as part of the the PRIN 2017 project n. 20173YP4N3. Publisher Copyright: © 2021, College Publications. All rights reserved. Copyright: Copyright 2021 Elsevier B.V., All rights reserved.

PY - 2021/3

Y1 - 2021/3

N2 - In this paper we lay the foundations of a new proof-theory for classical first-order logic that allows for a natural characterization of a notion of inferential depth. The approach we propose here aims towards extending the proof-theoretical framework presented in [6] by combining it with some ideas inspired by Hin-tikka’s work [18]. Unlike standard natural deduction, in this framework the inference rules that fix the meaning of the logical operators are symmetrical with respect to assent and dissent and do not involve the discharge of formulas. The only discharge rule is a classical dilemma rule whose nested applications provide a sensible measure of inferential depth. The result is a hierarchy of decidable depth-bounded approximations of classical first-order logic that ex-pands the hierarchy of tractable approximations of Boolean logic investigated in [11, 10, 7].

AB - In this paper we lay the foundations of a new proof-theory for classical first-order logic that allows for a natural characterization of a notion of inferential depth. The approach we propose here aims towards extending the proof-theoretical framework presented in [6] by combining it with some ideas inspired by Hin-tikka’s work [18]. Unlike standard natural deduction, in this framework the inference rules that fix the meaning of the logical operators are symmetrical with respect to assent and dissent and do not involve the discharge of formulas. The only discharge rule is a classical dilemma rule whose nested applications provide a sensible measure of inferential depth. The result is a hierarchy of decidable depth-bounded approximations of classical first-order logic that ex-pands the hierarchy of tractable approximations of Boolean logic investigated in [11, 10, 7].

UR - http://www.scopus.com/inward/record.url?scp=85111093513&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:85111093513

SN - 2631-9810

VL - 8

SP - 423

EP - 451

JO - IfCoLoG Journal of Logics and their Applications

JF - IfCoLoG Journal of Logics and their Applications

IS - 2

ER -

Towards depth-bounded natural deduction for classical first-order logic

Abstract

Other files and links

Fingerprint

Cite this