inria-00000698, version 1
Implementing Deep Inference in Tom
Ozan Kahramanogullari
1Pierre-Etienne Moreau
2Antoine Reilles
2
ICALP Workshop on Structures and Deduction (2005) 158--172
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.
- 1: Computer Science Institute, University of Leipzig
- Computer Science Institute – University of Leipzig
- 2: PROTHEO (INRIA Lorraine - LORIA)
- INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- Domain : Computer Science/Programming Languages
- Comment : ISSN 1430-211X
- inria-00000698, version 1
- http://hal.inria.fr/inria-00000698
- oai:hal.inria.fr:inria-00000698
- From: Pierre-Etienne Moreau
- Submitted on: Tuesday, 15 November 2005 09:35:27
- Updated on: Monday, 3 July 2006 15:19:34






Associated documents
Export