The system AxiomCalc takes as input an 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,
AxiomCalc automatically generates a LaTeX-document which contains the analytic
calculus extended with this axiom.
The input axiom should be specified in the language of Full Lambek Calculus with exchange and weakening FLew (i.e. intuitionistic logic without contraction).
AxiomCalc
For more information, please have a look at the tab "Using AxiomCalc"!
The input axiom may consist of:
a -> 1, 0 -> a, (a*a) -> a, -a v -(-a), (a -> b) v (b -> a), -(a*b) v (a&b -> a*b), ...
AxiomCalc 1.3 is available for free as a tarred archive:
In order to run AxiomCalc, enter your Prolog-environment from the directory axiomcalc1.2.2 and consult ac_kernl.pl.
$ swipl ?- [ac_kernl].
Start AxiomCalc by typing "compute." on the command-line. 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 commandline.
?- compute. |: -(a & -a). This axiom is in the class: n(2) Equivalent Analytic Rule: G+1,G+1 => ----------------------------- G+1 =>
To start AxiomCalc and check for the conditions on standard completeness, type "computesc" on the command-line. Also in this case, you're expected to provide some axiom. As a result, you get the equivalent analytic (hyper)sequent rule and some information on whether the conditions on standard completeness are met.
?- computesc. |: -(a*b) v (a&b -> a*b). This axiom is in the class: p(3) Equivalent Analytic Rule (in presence of the axiom (a -> b) v (b -> a)): G|G+1,G+1,D+1 => P+1 G|G+2,G+1,D+1 => P+1 G|G+2,G+3,D+1 => P+1 G|G+1,G+3,D+1 => P+1 ----------------------------- G| G+2,G+3 => | G+1,D+1 => P+1 The logic obtained by extending MTL with the axiom is standard complete.
Moreover, a LaTeX-document is automatically generated and can be found in
axiomcalc1.3/tex/AxiomCalc-Output.tex
axiomcalc1.3/tex/AxiomCalcSC-Output.tex
The input axiom may consist of:
a -> 1, 0 -> a, (a*a) -> a, -a v -(-a), -(a*b) v (a&b -> a*b)
The procedure to generate analytic (hyper)sequent rules equivalent to the Hilbert axioms in the input proceeds in two steps:
?- compute. |: (a -> b) v (b -> a). This axiom is in the class: p(2) Equivalent Analytic Rule: G|G+1,D+2 => P+2 G|G+2,D+1 => P+1 ----------------------------- G| D+2,G+2 => P+2| D+1,G+1 => P+1
G+i, D+j and P+k are fresh metavariables introduced during the completion procedure. They should be read as Γ_i, Δ_j and Π_k. i, j and k are indices.
The people currently involved in AxiomCalc are:
For more information, requests or suggestions, please contact Lara Spendier (lara [at] logic [dot] at), who is the author of AxiomCalc.