“SuperZenon is an experimental extension of the Zenon automated theorem prover, using the principles of superdeduction, among which the theory is used to enrich the deduction system with new deduction rules.
Superdeduction is a variant of deduction modulo, which is an extension of logical deduction systems consisting in canonically adding ad hoc deduction rules translating axiomatic theories. This has several advantages:
• Proofs are shorter, more readable, and close to the mathematical reasoning
• Automated proof search may speed up in such systems as some systematic parts of the proofs are ”compiled” into superdeduction rules.
A version of SuperZenon has been instantiated for the set theory of the B method. This allows us to provide another prover to Atelier B, which can be used to verify B proof rules in particular. This version of SuperZenon has been successfully applied (with significant speed-ups both in terms of proof time and proof size) to the verification of B proof rules coming from the database maintained by Siemens IC-MOL.”
David Delahaye, CEDRIC/CNAM, France
Source: CAD ATP System Competition (24th June 2012)