Karnak, An Automated Theorem Prover for PPC
Tarek Mohamed, Elnadi Albert Hoogewijs · 1995
In this paper we introduce KARNAK ? , an automated theorem prover for the partial predicate calculus PPC ? . PPC ? has been introduced in [8] as an equivalent logic for LPF, the Logic of Partial Functions which is the logical basis of the software specication language VDM [10]. KARNAK ? is used to show that a complete subsystem of LPF is derivable from PPC ? , and hence it follows that PPC ? is also complete. In addition, theorem preserving transformations between PPC and PPC ? are introduced.