TINC - Framinator

The system Framinator (FRAMe condItioNs Automatically TO Rules) takes as input a frame condition in the language of first-order classical logic provided by the user and transforms it — if possible — into an equivalent labelled rule according to the algorithm in [1]. The output of Framinator is a LaTeX-document which contains the cut-free labelled calculus for the considered logic.
The input formula should be a prenex formula in the language of first-order classical logic.

Framinator

  1. identifies the class of the arithmetical hierarchy to which the frame condition belongs,
  2. transforms the frame condition within the class Pi(2) of the arithmetical hierarchy into an equivalent structural labelled rule, and
  3. provides a paper containing a cut-free calculus for the logic defined by imposing the frame condition on the standard intuitionistic frame.

Input Syntax

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

The input formula is a formula in prenex normal form where the prefix is separated from the matrix with a ':', i.e.: (prefix):(matrix). The formula may consist of:

  • A for the universal and E for the existential quantifier
  • the letters [a-z] (except for v) for variables
  • the symbol < denoting the accessibility relation "<=" (less or equal)
  • logical connectives:
    • & ... and
    • v ... or
    • - ... negation
    • -> ... implication
Note that several frame conditions can be concatenated with an ';'.

Examples

  (A x A y A z E w):((x<y & x<z) -> (y<w & z<w)); (A x A y):(x<y -> y<x); (A x A y A z) : ((x<y & y<z) -> (y<x v z<y)) ...

Input Frame Condition:   
Check

Framinator 1.0 is available for free as a tarred archive:

Run Framinator

In order to run Framinator, enter your Prolog-environment from the directory framinator1.0 and consult f_kernl.pl. 

			   	$ swipl
			
			   	?- [f_kernl].

Start Framinator by typing "compute." on the command-line. Next, you're expected to provide some frame condition that should be transformed into a labelled rule. As a result, the equivalent labelled rules are printed on the commandline. 

			  	?- compute.
				|: (A x A y):(x<y -> y<x).

				The frame condition is in the class: p(1)

				Equivalent Labelled Rule(s): 
				 x<y,y<x,G => D       
				 -----------------------------
				 x<y,G => D

Moreover, a LaTeX-document is automatically generated and can be found in
   framinator1.0/ftex/Framinator-Output.tex

Input Syntax & Examples

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

The input formula is a formula in prenex normal form where the prefix is separated from the matrix with an ':', i.e.: (prefix):(matrix). The formula may consist of:

  • A for the universal and E for the existential quantifier
  • the letters [a-z] (except v) for variables
  • the symbol < denoting the accessibility relation "<=" (less or equal)
  • logical connectives:
    • & ... and
    • v ... or
    • - ... negation
    • -> ... implication
Note that several frame conditions can be concatenated with an ';'. Examples for frame conditions are: 
  (A x A y A z E w):((x < y & x <z) -> (y < w & z <w)); (A x A y):(x<y -> y<x); (A x A y A z) : ((x<y & y<z) -> (y<x v z<y)) ...

Output of Framinator

The procedure to generate labelled rules equivalent to the frame conditions in the input proceeds in two steps:

  1. The algorithm generates a structural rule for labelled calculus equivalent to the original frame condition.
  2. The generated rule is transformed into an equivalent rule that preserves cut-elimination when added to G3I. 
  
				  ?- compute.
				  |:    (A x A y A z E w):((x<y & x<z) -> (y<w & z<w)).

				  The frame condition is in the class: [p(2)]

				  Equivalent Labelled Rule(s): 

				    G => D,x<y      G => D,x<z      y<w,z<w,G => D       
    				    -----------------------------
				    G => D

G, and D are fresh metavariables introduced during the completion procedure (step (2)). They should be read as Gamma, and Delta.

  1. A. Ciabattoni, P. Maffezioli and L. Spendier, Hypersequent and Labelled Calculi for Intermediate Logics. In Proceedings of TABLEAUX 2013, D. Galmiche and D. Larchey-Wendling (Eds.), LNCS 8123, pp. 81--96, 2013.

The people currently involved in Framinator are:

For more information, requests or suggestions, please contact Lara Spendier (lara [at] logic [dot] at), who is the author of Framinator.