Nalazite se na CroRIS probnoj okolini. Ovdje evidentirani podaci neće biti pohranjeni u Informacijskom sustavu znanosti RH. Ako je ovo greška, CroRIS produkcijskoj okolini moguće je pristupi putem poveznice www.croris.hr
izvor podataka: crosbi

On multiple conclusion deductions in classical logic (CROSBI ID 244715)

Prilog u časopisu | izvorni znanstveni rad | međunarodna recenzija

Maretić, Marcel On multiple conclusion deductions in classical logic // Mathematical communications, 23 (2018), 1; 79-95

Podaci o odgovornosti

Maretić, Marcel

engleski

On multiple conclusion deductions in classical logic

Kneale observed that Gentzen’s calculus of natural deductions NK for classical logic is not symmetric and has unnecessarily complicated hypothetical inference rules. Kneale proposed inference rules with multiple conclusions as a basis for a symmetric natural deduction calculus for classical logic. However, Kneale’s informally presented calculus is not complete. In this paper, we define a calculus of multiple conclusion natural deductions (MCD) for classical propositional logic based on Kneale’s multiple conclusion inference rules. For MCD we present elementary proof search that produces proofs in normal form. MCD proof search is motivated and explained as being a notational variant of Smullyan’s analytic tableaux method in its initial part and a notational variant of refutation proofs based on Robinson’s resolution in its final part. We consider MCD to have semantic motivation of both its inference rules and its proof search. This is unusual for the natural deduction calculi as they are syntactically motivated. Syntactic motivation is adequate for intuitionistic logic but not a natural fit for truth-functional classical propositional logic.

multiple conclusion natural deductions ; Kneale's developments ; analytic deductions ; classical propositional logic

nije evidentirano

nije evidentirano

nije evidentirano

nije evidentirano

nije evidentirano

nije evidentirano

Podaci o izdanju

23 (1)

2018.

79-95

objavljeno

1331-0623

1848-8013

Trošak objave rada u otvorenom pristupu

APC

Povezanost rada

Matematika

Poveznice
Indeksiranost