TINC - AxiomCalc

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

  1. 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 preserving cut-elminiation when added to FLew (analytic rule)
    2. transforms each axiom within the class P3 into an equivalent structural hypersequent rule preserving cut-elimination when added to the hypersequent version of FLew (analytic rule),
  3. provides a paper containing an analytic calculus for FLew (a hypersequent version for FLew, resp.) extended with the axiom, and
  4. (if explicitely required by the user) checks whether Monoidal T-norm Logic MTL extended with the input axiom is standard complete.

Input Syntax

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

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 ... or
    • * ... fusion/multiplicative and
    • - ... negation
    • -> ... implication

Examples

  a -> 1, 0 -> a, (a*a) -> a, -a v -(-a), (a -> b) v (b -> a), -(a*b) v (a&b -> a*b), ...

Input Axiom:    Check for Standard Completeness
Check

AxiomCalc 1.3 is available for free as a tarred archive:

Run AxiomCalc

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

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 ... or
    • * ... fusion/multiplicative and
    • - ... negation
    • -> ... implication
Examples for axioms are: 
  a -> 1, 0 -> a, (a*a) -> a, -a v -(-a), -(a*b) v (a&b -> a*b)

Output of AxiomCalc

The procedure to generate analytic (hyper)sequent rules equivalent to the Hilbert axioms in the 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 FLew for (hyper)sequents. 
  
				  ?- 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.

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

  2. P. Baldi, A. Ciabattoni and L. Spendier. Standard Completeness for Extensions of MTL: an Automated Approach. Workshop on Logic, Language, Information and Computation, LNCS 7456, pp. 154--167, 2012.

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.