TINC - InvAxiomCalc

General Information
InvAxiomCalc Web Interface
Obtaining InvAxiomCalc
Using InvAxiomCalc
References
Contact

The system InvAxiomCalc takes as input a Hilbert-style axiom provided by the user and transforms it - if possible - into an equivalent analytic sequent or hypersequent rule according to the algorithm in [1]. Moreover, InvAxiomCalc automatically generates a LaTeX-document which contains the analytic calculus extended with this axiom.
The input axiom should be specified in the language of classical linear logic without exponentials (i.e. Multiplicative Additive Linear Logic MALL).

InvAxiomCalc

identifies to which class in the substructural hierarchy of [1] the axiom belongs to
1. transforms each axiom within the class N2 into an equivalent structural sequent rule
2. transforms each axiom within the class P'3 into an equivalent structural hypersequent rule
3. checks the acyclicity condition as defined in [1] for the generated structural sequent or hypersequent rules
4. transforms each structural sequent rule satisfying the acyclicity condition into analytic rule (i.e. rule preserving cut-elimination) when added to MALL
5. transforms each structural hypersequent rule satisfying the acyclicity condition into an equivalent analytic rule (i.e. rule preserving cut-elimination) when added to HMALL - a hypersequent version of MALL
provides a paper containing an analytic calculus for HMALL (a hypersequent version for MALL, resp.) extended with the axiom.

Input Syntax

For more information, please have a look at the tab "Using InvAxiomCalc"!

The input axiom may consist of:

the letters [a-z] for atomic formulas
0, 1, bot and top for logical constants
logical connectives:
- & ... additive and (&)
- v ... additive or (oplus)
- * ... multiplicative and (otimes)
- - ... linear negation (nil)
- + ... multiplicative or (par)

Examples

                          a v (-a + -a + -a), a + 1, -a + (a * a), (-a + b) v (-b + a), ...

InvAxiomCalc is available for free as a tarred archive:

InvAxiomCalc: Available from InvAxiomCalc-[VERSION].tar. It is written in Prolog. For more information see also the README-file in the package.
Prolog: In order to run InvAxiomCalc, you also need a standard Prolog system. Download e.g. SWI-Prolog (by Jan Wielemaker), which is freely available from www.swi-prolog.org
TeX-System: To enjoy the pretty paper InvAxiomCalc generates based on your input, you'll need LaTeX installed on your system.

Run InvAxiomCalc

In order to run InvAxiomCalc, enter your Prolog-environment from the directory invaxiomcalc-[VERSION] and consult invac_kernel.pl.

                          $ swipl

                          ?- [invac_kernel].

Start InvAxiomCalc by typing "compute." on the terminal. Next, you're expected to provide some axiom that should be transformed into an analytic rule. As a result, the equivalent analytic sequent or hypersequent rules are printed on the terminal.

                          ?- compute.
                          |: (-a + b) v (-b + a).

                          This axiom is in the class: p(2)


                          Equivalent Analytic Rule:

                           H|  |- ['Y'+2,'Y'+3]      H|  |- ['Y'+4,'Y'+1]
                          ______________________________________________________________
                                 H|  |- ['Y'+3,'Y'+4] |  |- ['Y'+1,'Y'+2]

Moreover, a LaTeX-document is automatically generated and can be found in:
invaxiomcalc-[VERSION]/tex/InvAxiomCalc-Output.tex

Input Syntax & Examples

The input axiom may consist of:

the letters [a-z] for atomic formulas
0, 1, bot and top for logical constants
logical connectives:
- & ... additive and (&)
- v ... additive or (oplus)
- * ... multiplicative and (otimes)
- - ... linear negation (nil)
- + ... multiplicative or (par)

Examples for axioms are:

 a v (-a + -a + -a), a + 1, -a + (a * a), (-a + b) v (-b + a), ...

Output of InvAxiomCalc

The procedure to generate analytic (hyper)sequent rules equivalent to the Hilbert axioms provided as input proceeds in two steps:

The algorithm generates a structural rule in (hyper)sequent calculus equivalent to the original axiom.
The generated rule is transformed into an equivalent analytic rule that preserves cut-elimination when added to MALL for (hyper)sequents.

                    				  ?- compute.
                    				  |: (-a + b) v (-b + a).

                              This axiom is in the class: p(2)


                              Equivalent Analytic Rule:

                               H|  |- ['Y'+2,'Y'+3]      H|  |- ['Y'+4,'Y'+1]
                              ______________________________________________________________
                                     H|  |- ['Y'+3,'Y'+4]|  |- ['Y'+1,'Y'+2]

'Y'+1, 'Y'+2, 'Y'+3 and 'Y'+4 are fresh metavariables introduced during the completion procedure. They should be read as Γ, Δ, Σ and Θ.

A. Ciabattoni, L. Strassburger, and K. Terui, Expanding the realm of systematic proof theory, Proceedings of Computer Science Logic, LNCS 5771, pp. 163--178, 2009.
A. Ciabattoni, N. Galatos and K. Terui, From axioms to analytic rules in nonclassical logics. IEEE Symposium on Logic in Computer Science (LICS'08) , IEEE pp. 229-240, 2008.

The people currently involved in InvAxiomCalc are:

For more information, requests or suggestions, please contact Ardit Ymeri, who is the author of InvAxiomCalc.