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
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 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)) ...
Framinator 1.0 is available for free as a tarred archive:
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
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 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)) ...
The procedure to generate labelled rules equivalent to the frame conditions in the input proceeds in two steps:
?- 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.
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.