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.
Document type :
Conference papers
Liste complète des métadonnées

https://hal.inria.fr/inria-00098715
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:19:17 AM
Last modification on : Thursday, January 11, 2018 - 6:19:58 AM
Document(s) archivé(s) le : Wednesday, March 29, 2017 - 12:30:41 PM

Identifiers

  • 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, F. Pfenning, B. Gramlich, 1998, Lindau, Germany, pp.23-34. ⟨inria-00098715⟩

Share

Metrics

Record views

84

Files downloads

47