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

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

Input Axiom:   

InvAxiomCalc is available for free as a tarred archive:

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:

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