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

Hans De Nivelle

doi:10.1093/logcom/exu071

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

Hans De Nivelle

University of Wrocław

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

2 Citations (Scopus)

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.

Original language	English
Pages (from-to)	509-548
Number of pages	40
Journal	Journal of Logic and Computation
Volume	27
Issue number	2
DOIs	https://doi.org/10.1093/logcom/exu071
Publication status	Published - Mar 2017
Externally published	Yes

Keywords

Automated theorem proving
Finite model search
Partial functions
Sequent calculus
Three-valued logic

ASJC Scopus subject areas

Theoretical Computer Science
Software
Arts and Humanities (miscellaneous)
Hardware and Architecture
Logic

Access to Document

10.1093/logcom/exu071

Cite this

@article{df3befab222244259db8521bcb607b29,

title = "Theorem proving for classical logic with partial functions by reduction to Kleene logic",

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.",

keywords = "Automated theorem proving, Finite model search, Partial functions, Sequent calculus, Three-valued logic",

author = "\{De Nivelle\}, Hans",

note = "Publisher Copyright: {\textcopyright} The Author, 2014.",

year = "2017",

month = mar,

doi = "10.1093/logcom/exu071",

language = "English",

volume = "27",

pages = "509--548",

journal = "Journal of Logic and Computation",

issn = "0955-792X",

publisher = "Oxford University Press",

number = "2",

}

TY - JOUR

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

AU - De Nivelle, Hans

N1 - Publisher Copyright: © The Author, 2014.

PY - 2017/3

Y1 - 2017/3

N2 - 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.

AB - 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.

KW - Automated theorem proving

KW - Finite model search

KW - Partial functions

KW - Sequent calculus

KW - Three-valued logic

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

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

U2 - 10.1093/logcom/exu071

DO - 10.1093/logcom/exu071

M3 - Article

AN - SCOPUS:85018287166

SN - 0955-792X

VL - 27

SP - 509

EP - 548

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

IS - 2

ER -

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

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this