Applying semantic subsumption rules in the context of inductive proofs

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 : Due to the inherent incompleteness of the inductive proof methods, they should be combined with other methods more suitable to reason on specific domains. In the paper, it is shown how the standard inference system of SPIKE theorem prover can be extended with semantic subsumption rules in order to facilitate a better integration of other reasoning modules.
Type de document :
Communication dans un congrès
Workshop on Integration of Deductive Systems - CADE-15, 1998, none, 11 p, 1998
Liste complète des métadonnées

https://hal.inria.fr/inria-00098496
Contributeur : Publications Loria <>
Soumis le : lundi 25 septembre 2006 - 17:02:04
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • HAL Id : inria-00098496, version 1

Collections

Citation

Sorin Stratulat. Applying semantic subsumption rules in the context of inductive proofs. Workshop on Integration of Deductive Systems - CADE-15, 1998, none, 11 p, 1998. 〈inria-00098496〉

Partager

Métriques

Consultations de la notice

86