Implementing Deep Inference in Tom

Abstract : The calculus of structures is a proof theoretical formalism which generalizes sequent calculus with the feature of deep inference: in contrast to sequent calculus, the calculus of structures does not rely on the notion of main connective and, like in term rewriting, it permits the application of the inference rules at any depth inside a formula. Tom is a pattern matching processor that integrates term rewriting facilities into imperative languages. In this paper, relying on the correspondence between the systems in the calculus of structures and term rewriting systems, we present an implementation of system BV of the calculus of structures in Java by exploiting the term rewriting features of Tom. This way, by means of the expressive power due to Java, it becomes possible to implement different search strategies. Since the systems in the calculus of structures follow a common scheme, we argue that our implementation can be generalized to other systems in the calculus of structures for classical logic, modal logics, and different fragments of linear logic.
Document type :
Conference papers
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/inria-00000698
Contributor : Pierre-Etienne Moreau <>
Submitted on : Tuesday, November 15, 2005 - 9:35:27 AM
Last modification on : Saturday, November 24, 2018 - 2:04:22 PM
Long-term archiving on: Tuesday, September 11, 2012 - 12:52:11 PM

Identifiers

  • HAL Id : inria-00000698, version 1

Collections

Citation

Ozan Kahramanogullari, Pierre-Etienne Moreau, Antoine Reilles. Implementing Deep Inference in Tom. ICALP Workshop on Structures and Deduction, May 2005, Lisbon/Portugal, pp.158--172. ⟨inria-00000698⟩

Share

Metrics

Record views

234

Files downloads

106