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
For more information, please have a look at the tab "Using InvAxiomCalc"!
The input axiom may consist of:
[a-z]
for atomic formulas 0
, 1
, bot
and top
for logical constants &
... additive and (&) v
... additive or (oplus) *
... multiplicative and (otimes) -
... linear negation (nil) +
... multiplicative or (par)
a v (-a + -a + -a), a + 1, -a + (a * a), (-a + b) v (-b + a), ...
InvAxiomCalc is available for free as a tarred archive:
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
The input axiom may consist of:
[a-z]
for atomic formulas 0
, 1
, bot
and top
for logical constants &
... additive and (&) v
... additive or (oplus) *
... multiplicative and (otimes) -
... linear negation (nil) +
... multiplicative or (par) a v (-a + -a + -a), a + 1, -a + (a * a), (-a + b) v (-b + a), ...
The procedure to generate analytic (hyper)sequent rules equivalent to the Hilbert axioms provided as input proceeds in two steps:
?- 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 Θ.
The people currently involved in InvAxiomCalc are: