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 |
