# TINC - InvAxiomCalc

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 . 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  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  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

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), ...
```

Input Axiom:

• 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:

1. The algorithm generates a structural rule in (hyper)sequent calculus equivalent to the original axiom.
2. 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 Θ.

1. 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.
2. 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: