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

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 metadata

Cited literature [19 references]  Display  Hide  Download

Contributor : Pierre-Etienne Moreau Connect in order to contact the contributor
Submitted on : Tuesday, November 15, 2005 - 9:35:27 AM
Last modification on : Friday, February 4, 2022 - 3:31:59 AM
Long-term archiving on: : Tuesday, September 11, 2012 - 12:52:11 PM


  • HAL Id : inria-00000698, version 1



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⟩



Record views


Files downloads