Clausal Presentation of Theories in Deduction Modulo

Jianhua Gao 1, 2
1 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : 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.
Type de document :
Communication dans un congrès
PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Aug 2011, Wroclaw, Poland. 2011
Liste complète des métadonnées

Littérature citée [8 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00614251
Contributeur : Assia Mahboubi <>
Soumis le : mercredi 10 août 2011 - 12:47:31
Dernière modification le : jeudi 10 mai 2018 - 02:06:30
Document(s) archivé(s) le : vendredi 11 novembre 2011 - 02:21:00

Fichier

Gao.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00614251, version 1

Collections

Citation

Jianhua Gao. Clausal Presentation of Theories in Deduction Modulo. PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Aug 2011, Wroclaw, Poland. 2011. 〈inria-00614251〉

Partager

Métriques

Consultations de la notice

393

Téléchargements de fichiers

151