|
 
|
[Del13] Automated Deduction Modulo
Conférences invitées : Proof-Search in Axiomatic Theories and Type Theories (PSATTT), November 2013, pp.online, Palaiseau, France,Mots clés: Deduction Modulo, Superdeduction, Automated Theorem Proving, Proof Compression, Proof Verification, Zenon, Dedukti
Résumé:
This talk is about several experiments of automated deduction with deduction modulo. The theory of deduction modulo is an extension of predicate calculus, which allows us to rewrite terms as well as propositions, and which is well suited for proof search in axiomatic theories, as it turns axioms into rewrite rules. In particular, we present two extensions of the Zenon tableau-based first order automated theorem prover to deduction modulo, called Zenon Modulo (a direct extension to deduction modulo) and Super Zenon (an extension to superdeduction, a variant of deduction modulo). These extensions do not only improve Zenon, but also seem quite appropriate for automated deduction in set theory, where difficult problems can be proved by these extensions. These results are particularly promising, as we aim to consider the set theory of the B method, in order to apply these extensions to the verification of proof obligations coming from industrial applications, which is one of the goals of the BWare project.
Equipe:
sys
BibTeX
| @inproceedings { | |||
| Del13, | |||
| title | = | "{Automated Deduction Modulo}", | |
| author | = | " D. Delahaye ", | |
| booktitle | = | "{Proof-Search in Axiomatic Theories and Type Theories (PSATTT)}", | |
| year | = | 2013, | |
| month | = | "November", | |
| pages | = | "online", | |
| address | = | "Palaiseau, France", | |
| } | |||
