HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/inria-00165997
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Tuesday, July 31, 2007 - 10:13:38 AM
Last modification on : Thursday, January 20, 2022 - 5:30:45 PM
Long-term archiving on: : Friday, April 9, 2010 - 12:14:24 AM

File

CharMedial.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

174

Files downloads

64