View in EDS PDF Full Text

On multiple conclusion deductions in classical logic.

Saved in:
Bibliographic Details
Title: On multiple conclusion deductions in classical logic.
Authors: MARETIĆ, MARCEL1 marcel.maretic@foi.hr
Source: Mathematical Communications. 2018, Vol. 23 Issue 1, p79-95. 17p.
Subjects: Calculus, Natural deduction (Logic), Intuitionistic mathematics, Linear differential equations, Nonlinear equations
Abstract: 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. AMS subject classifications: 03B05, 03F03 [ABSTRACT FROM AUTHOR]
Copyright of Mathematical Communications is the property of University of Osijek, Department of Mathematics and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Links:
  – Type: pdflink
Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 127633657
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: On multiple conclusion deductions in classical logic.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22MARETIĆ%2C+MARCEL%22">MARETIĆ, MARCEL</searchLink><relatesTo>1</relatesTo><i> marcel.maretic@foi.hr</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Mathematical+Communications%22">Mathematical Communications</searchLink>. 2018, Vol. 23 Issue 1, p79-95. 17p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Calculus%22">Calculus</searchLink><br /><searchLink fieldCode="DE" term="%22Natural+deduction+%28Logic%29%22">Natural deduction (Logic)</searchLink><br /><searchLink fieldCode="DE" term="%22Intuitionistic+mathematics%22">Intuitionistic mathematics</searchLink><br /><searchLink fieldCode="DE" term="%22Linear+differential+equations%22">Linear differential equations</searchLink><br /><searchLink fieldCode="DE" term="%22Nonlinear+equations%22">Nonlinear equations</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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. AMS subject classifications: 03B05, 03F03 [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Mathematical Communications is the property of University of Osijek, Department of Mathematics and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=127633657
RecordInfo BibRecord:
  BibEntity:
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 17
        StartPage: 79
    Subjects:
      – SubjectFull: Calculus
        Type: general
      – SubjectFull: Natural deduction (Logic)
        Type: general
      – SubjectFull: Intuitionistic mathematics
        Type: general
      – SubjectFull: Linear differential equations
        Type: general
      – SubjectFull: Nonlinear equations
        Type: general
    Titles:
      – TitleFull: On multiple conclusion deductions in classical logic.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: MARETIĆ, MARCEL
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 01
              Text: 2018
              Type: published
              Y: 2018
          Identifiers:
            – Type: issn-print
              Value: 13310623
          Numbering:
            – Type: volume
              Value: 23
            – Type: issue
              Value: 1
          Titles:
            – TitleFull: Mathematical Communications
              Type: main
ResultId 1