s'authentifier
version française rss feed

inria-00614251, version 1

Clausal Presentation of Theories in Deduction Modulo

Jianhua Gao 12

PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories (2011)

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.

  • Domaine : Informatique/Logique en informatique
 
  • inria-00614251, version 1
  • oai:hal.inria.fr:inria-00614251
  • Contributeur : 
  • Soumis le : Mercredi 10 Août 2011, 12:47:31
  • Dernière modification le : Jeudi 11 Août 2011, 14:22:08
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...