A General Framework to Build Multi-logic Implicit Induction Provers

Sorin Stratulat 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Cover sets are at the core of implicit induction proof techniques which keep the advantages of explicit induction and proof by consistency. Contextual cover sets are a generalized form of them since they can be generated also with the help of 'not yet certified' information that can be however soundly used in the deduction process. In a first step, we present an abstract inference system as our general framework to build implicit induction provers. Compared with other similar inference systems, the new soundness proof arguments allowed us to weaken the applicability conditions of the inference rules and augment their simplification capabilities. Contextual cover sets are implemented by (combinations of) reasoning modules that may have different reasoning domains or deduction methods other than induction. In a second step, we present a generic and sound integration schema of reasoning modules inside our framework. As a case study, we define a set of reasoning modules for conditional theories based on rewriting techniques and we define the inference system of $Spike$ in terms of them. Finally, we propose extensions of it by introducing new reasoning modules for linear arithmetic or based on semantic subsumption. We give as example the application of an extended version of $Spike$ to prove the correctness of the MJRTY algorithm by performing a combination of inductive and arithmetic reasoning.
Type de document :
Rapport
[Intern report] 99-R-310 || stratulat99a, 1999, 32 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00098939
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:40:30
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • HAL Id : inria-00098939, version 1

Collections

Citation

Sorin Stratulat. A General Framework to Build Multi-logic Implicit Induction Provers. [Intern report] 99-R-310 || stratulat99a, 1999, 32 p. 〈inria-00098939〉

Partager

Métriques

Consultations de la notice

161