Theorem Proving in PCL Partial Classical Logic (PCL) is a three-valued logic that I introduced in 2009-2010 with the goal of modelling partial functions in mathematics and programming. In 2012, I developed theorem proving methods for PCL, based on geometric logic. I turned out that these theorem proving methods are not just a collection of tricks, but that they provide some real insight into the nature of PCL. It let to the following indirect results: - A clarification of the relation between classical logic, PCL and 3-valued Kleene logic. - A new calculus Seq(\preceq) for PCL, with a somewhat unusual semantics, which has more readable and shorter proofs than its predecessor (Seq2PCL). And of course, I will explain how to do the theorem proving: First translate PCL into Kleene logic, and after that use any of the standard techniques (resolution, semantic tableaux, geometric logic) with minimal adaptation.