KARNAK an automated theorem prover for PPC. Elnadi, Tarek Mohamed, Hoogewijs, Albert (1995) Bulletin of the Belgian Mathematical Society - Simon Stevin