Theorem proving for classical logic with partial functions by reduction to Kleene logic
Hans de Nivelle · Journal of Logic and Computation · 2014
Partial functions are abundant in mathematics and program specifications. Unfortunately, their importance has been mostly ignored in automated theorem proving. In this paper, 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 equivalentsetsofformulas inKleenelogic. Forproofsearchweuseathree-valued adaptation of geometric resolution. We prove that the calculus is sound and complete.