Skip to Main content Skip to Navigation
New interface
Conference papers

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
Complete list of metadata
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 8:19:17 AM
Last modification on : Friday, February 4, 2022 - 3:32:00 AM
Long-term archiving on: : Wednesday, March 29, 2017 - 12:30:41 PM


  • HAL Id : inria-00098715, version 1



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⟩



Record views


Files downloads