Clausal Presentation of Theories in Deduction Modulo - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2011

Clausal Presentation of Theories in Deduction Modulo

Résumé

Resolution modulo is an extension of first-order resolution where axioms are replaced by rewrite rules, used to rewrite, or more generally narrow, clauses during the search. In the first version of this method, clauses were rewritten to arbitrary propositions, that needed to be dynamically transformed into clauses. This unpleasant feature can be eliminated when the rewrite system is clausal, i.e. when it transforms clauses to clauses. We show in this paper that how to transform any rewrite system into a clausal one, preserving the existence of cut free proof of any sequent.
Fichier principal
Vignette du fichier
Gao.pdf (165.88 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00614251 , version 1 (10-08-2011)

Identifiants

  • HAL Id : inria-00614251 , version 1

Citer

Jianhua Gao. Clausal Presentation of Theories in Deduction Modulo. PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Germain Faure, Stéphane Lengrand, Assia Mahboubi, Aug 2011, Wroclaw, Poland. ⟨inria-00614251⟩
127 Consultations
164 Téléchargements

Partager

Gmail Facebook X LinkedIn More