Using Rewriting and Strategies for Describing the B Predicate ProverReportar como inadecuado




Using Rewriting and Strategies for Describing the B Predicate Prover - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

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.

keyword : règle de réécriture predicate calculus rewrite rule strategy stratégie calcul de predicat





Autor: Horatiu Cirstea - Claude Kirchner -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados