In this talk we will first give a short introduction to the Partial Predicate Logic (PPC). The 3-valued logic PPC is developed by Prof. A. Hoogewijs at the University of Ghent and is still under development. The last modification, PPC*, is compatible with the Logic for Partial Functions of Barringer, Cheng and Jones (LPF).
The difference between PPC and LPF is the definition of validity. Where BCJ presume that a formula is valid iff the formula is true for a model, PPC define that a formula is valid iff the formula in not false, which means true or undefined.
Secondly, we will demonstrate the trials and errors of using Isabelle to implement PPC, from building a new theory, over deducing new rules, to goal-directed proofmethods. Up to now, we constructed a minimal PPC without quantifiers.