Manfred Kerber, Michael Kohlhase

• Even though it is not very often admitted, partial functionsdo play a significant role in many practical applications of deduction sys-tems. Kleene has already given a semantic account of partial functionsusing a three-valued logic decades ago. This approach allows rejectingcertain unwanted formulae as faulty, which the simpler two-valued onesaccept. We have developed resolution and tableau calculi for automatedtheorem proving that take the restrictions of the three-valued logic intoaccount, which however have the severe drawback that existing theo-rem provers cannot directly be adapted to the technique. Even recentlyimplemented calculi for many-valued logics are not well-suited, since inthose the quantification does not exclude the undefined element. In thiswork we show, that it is possible to enhance a two-valued theorem proverby a simple strategy so that it can be used to generate proofs for the the-orems of the three-valued setting. By this we are able to use an existingtheorem prover for a large fragment of the language.