Using Rewriting and Strategies for Describing the B Predicate Prover

Horatiu Cirstea 1 Claude Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The framework of computational systems has been already used for describing several computational logics. In this paper is described the way a propositional prover and a predicate prover are implemented in ELAN, the system developed in Nancy for describing and executing computational systems. The inference rules for the provers are described by conditional rewrite rules and their application is controlled by strategies. We show how different strategies using the same set of rewrite rules can yield different proof methods.
Type de document :
Communication dans un congrès
Proceedings of the Workshop on Strategies in Automated Deduction - CADE-15, 1998, Lindau, Germany, pp.23-34, 1998
Liste complète des métadonnées

https://hal.inria.fr/inria-00098715
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:19:17
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : mercredi 29 mars 2017 - 12:30:41

Fichiers

Identifiants

  • HAL Id : inria-00098715, version 1

Collections

Citation

Horatiu Cirstea, Claude Kirchner. Using Rewriting and Strategies for Describing the B Predicate Prover. Proceedings of the Workshop on Strategies in Automated Deduction - CADE-15, 1998, Lindau, Germany, pp.23-34, 1998. 〈inria-00098715〉

Partager

Métriques

Consultations de la notice

70

Téléchargements de fichiers

30