View in EDS PDF Full Text

Theorem proving for classical logic with partial functions by reduction to Kleene logic.

Saved in:
Bibliographic Details
Title: Theorem proving for classical logic with partial functions by reduction to Kleene logic.
Authors: DE NIVELLE, HANS1 nivelle@ii.uni.wroc.pl
Source: Journal of Logic & Computation. Mar2017, Vol. 27 Issue 2, p509-548. 40p.
Subjects: Automatic theorem proving, Artificial intelligence, Proof theory, Calculus, Mathematical analysis
Abstract: Partial functions are abundant in mathematics and programme specifications. Unfortunately, their importance has been mostly ignored in automated theorem proving. In this article, we develop a theorem proving strategy for Partial Classical Logic (PCL). Proof search takes place in Kleene Logic. We show that PCL theories can be translated into equivalent sets of formulas in Kleene logic. For proof search, we use a three-valued adaptation of geometric resolution. We prove that the calculus is sound and complete. [ABSTRACT FROM AUTHOR]
Copyright of Journal of Logic & Computation is the property of Oxford University Press / USA 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: 121940422
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Theorem proving for classical logic with partial functions by reduction to Kleene logic.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22DE+NIVELLE%2C+HANS%22">DE NIVELLE, HANS</searchLink><relatesTo>1</relatesTo><i> nivelle@ii.uni.wroc.pl</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Journal+of+Logic+%26+Computation%22">Journal of Logic & Computation</searchLink>. Mar2017, Vol. 27 Issue 2, p509-548. 40p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Automatic+theorem+proving%22">Automatic theorem proving</searchLink><br /><searchLink fieldCode="DE" term="%22Artificial+intelligence%22">Artificial intelligence</searchLink><br /><searchLink fieldCode="DE" term="%22Proof+theory%22">Proof theory</searchLink><br /><searchLink fieldCode="DE" term="%22Calculus%22">Calculus</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+analysis%22">Mathematical analysis</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Partial functions are abundant in mathematics and programme specifications. Unfortunately, their importance has been mostly ignored in automated theorem proving. In this article, we develop a theorem proving strategy for Partial Classical Logic (PCL). Proof search takes place in Kleene Logic. We show that PCL theories can be translated into equivalent sets of formulas in Kleene logic. For proof search, we use a three-valued adaptation of geometric resolution. We prove that the calculus is sound and complete. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Journal of Logic & Computation is the property of Oxford University Press / USA 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=121940422
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1093/logcom/exu071
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 40
        StartPage: 509
    Subjects:
      – SubjectFull: Automatic theorem proving
        Type: general
      – SubjectFull: Artificial intelligence
        Type: general
      – SubjectFull: Proof theory
        Type: general
      – SubjectFull: Calculus
        Type: general
      – SubjectFull: Mathematical analysis
        Type: general
    Titles:
      – TitleFull: Theorem proving for classical logic with partial functions by reduction to Kleene logic.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: DE NIVELLE, HANS
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 03
              Text: Mar2017
              Type: published
              Y: 2017
          Identifiers:
            – Type: issn-print
              Value: 0955792X
          Numbering:
            – Type: volume
              Value: 27
            – Type: issue
              Value: 2
          Titles:
            – TitleFull: Journal of Logic & Computation
              Type: main
ResultId 1