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 <>
Submitted on : Tuesday, July 31, 2007 - 10:13:38 AM
Last modification on : Thursday, January 7, 2021 - 3:40:14 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

301

Files downloads

123