A Characterisation of Medial as Rewriting Rule

Lutz Straßburger 1, 2
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : Medial is an inference rule scheme that appears in various deductive systems based on deep inference. In this paper we investigate the properties of medial as rewriting rule independently from logic. We present a graph theoretical criterion for checking whether there exists a medial rewriting path between two formulas. Finally, we return to logic and apply our criterion for giving a combinatorial proof for a decomposition theorem, i.e., proof theoretical statement about syntax.
Type de document :
Communication dans un congrès
RTA 2007, Jun 2007, Paris, France
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00165997
Contributeur : Lutz Straßburger <>
Soumis le : mardi 31 juillet 2007 - 10:13:38
Dernière modification le : jeudi 12 avril 2018 - 01:47:42
Document(s) archivé(s) le : vendredi 9 avril 2010 - 00:14:24

Fichier

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

Identifiants

  • HAL Id : inria-00165997, version 1

Collections

Citation

Lutz Straßburger. A Characterisation of Medial as Rewriting Rule. RTA 2007, Jun 2007, Paris, France. 〈inria-00165997〉

Partager

Métriques

Consultations de la notice

263

Téléchargements de fichiers

77