zbMATH — the first resource for mathematics

Theorem proving for classical logic with partial functions by reduction to Kleene logic. (English) Zbl 1444.03014
Summary: 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.

03B35 Mechanization of proofs and logical operations
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Full Text: DOI