TINC - Framinator

The system Framinator 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]. Moreover, Framinator automatically generates a LaTeX-document which contains the cut-free labelled calculus and some theoretical results.
The input formula should be specified in the language of first-order classical logic.

Framinator

  1. identifies to which class in the hierarchy of [1] the frame condition belongs to,
  2. transforms each frame condition within the class p(2) into an equivalent structural labelled rule preserving cut-elimination when added to G3I, and
  3. provides a paper containing a cut-free calculus for G3I extended with the frame conditions.

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.