cl-banner

FORT 1.0


Description

---------------------------------------------------------------------------

HELP

Type

	java -jar fort.jar -h

to get exactly this usage text.

---------------------------------------------------------------------------

VERSION

Type

	java -jar fort.jar -v

to get the version of FORT.

---------------------------------------------------------------------------

DECISION TOOL

In order to use FORT as a decision tool type:

	java -jar fort.jar -D []  ""

The  specifies the property that should be tested on the TRS
specified in . The syntax of TRSs follows the standard TPDB format.
As optional  the user may specify the verbosity level with
-v , where  takes a value in { 0, 1, 2 }. The higher the number
the more detailed the output will be. The default is 0 and just prints
the answer (YES, NO or MAYBE). Additionally a timeout can be defined
via -t , where the natural number  is interpreted as seconds.
The syntax of  is explained below. The quotation marks surrounding
it are essential.

---------------------------------------------------------------------------

SYNTHESIS TOOL

There are two ways to call the synthesis tool. The first one

	java -jar fort.jar -S [] ""

specifies the formula on the command line. The search space is restricted
by the following optional parameters ():

    -f 
    -v 
    -r " - "
    -s 
    -d 

The signature  is specified as a comma separated list of function
symbols and arities. For example, (a 0, g 1, h 1) specifies a constant a
and two unary symbols g and h. If no signature or is given, FORT will
incrementally increase the signature starting from a single constant.
The other optional parameters are the maximum number  of different
variables, the minimum and the maximum number of rewrite rules  and
, and the maximum size  and depth  of terms in the rewrite rules.
The default values are  = 1,  = 0,  = max{R1, 3},  = 4, and
 =  - 1. You may also specify " -", "- ", or "" for -r,
which specifies only the minimum, the maximum, or the fixed number of
rules, respectively.

The second way to call the synthesis tool

	java -jar fort.jar -S 

requires a  containing a line

    (FORMULA )

and optional lines

    (FUN )
    (VARIABLES )
    (RULES " - ")
    (SIZE )
    (DEPTH )

corresponding to the optional parameters described above.

---------------------------------------------------------------------------

SYNTAX OF FORMULAS

The syntax for  is given by the following EBNF:

     = 
              |   
              | '~'
              | (  )
              |  ()
  = '&' | '|' | '=>'
    = '->' | '->+' | '->*' | '->!' | '-||->' | '->e' | '->be'
              | '<-' | '+<-' | '*<-' | '<-!' | '<-||-' | 'e<-' | 'be<-'
              | '<->' | '<->*' | 'join' | 'meet' | '='
  = forall | exists
    = CR | WCR | SCR | SCR() | WN | UN | UN()
              | UNC | NFP | SN | diamond | diamond()
              | GCR | GWCR | WSCR | GSCR() | GUN | GUN()
              | GUNC | GNFP | Gdiamond | Gdiamond()
              | CR() | WCR() | SCR()
              | SCR(, ) | WN() | UN()
              | UN(, ) | NFP() | SN()
              | diamond() | diamond(, )
              | NF() | Fin(, )
    = 
              | '~'()
              | (  )
     = '->' | '-||->'

Here  is any nonempty sequence of alphanumeric symbols.
The formula must be closed.

---------------------------------------------------------------------------

SEMANTICS OF FORMULAS

The meaning of the terminal symbols in the above EBNF is explained here.

    '~'      negates the formula following it
    '&'      denotes conjunction
    '|'      denoted disjunction
    '=>'     denotes implication

The usual binding precedence '~' > '&' > '|' > '=>' is adopted. The
following binary rewrite relations (and their inverses) can be used:

    '->'       one-step rewriting
    '->+'      transitive closure of '->'
    '->*'      transitive reflexive closure of '->'
    '->!'      rewriting to normal form
    '-||->'    parallel rewriting
    '->e'      one-step rewriting at the root
    '->be'     one-step rewriting below the root
    '<->'      one-step bidirectional rewriting
    '<->*'     conversion
    'join'     joinability
    'meet'     meetability
    '='        equality

The following properties can be used:

    CR   confluence (Church-Rosser property)
         "~exists s, t, u (t <- s ->* u & ~t join u)"

    WCR  local confluence (weak Church-Rosser property)
         "~exists s, t, u (t <- s -> u & ~t join u)"

    SCR  strong confluence
         "~exists s, t, u (t <- s -> u & ~exists v (t ->= v & u ->* v))"

    SCR()
         strong confluence with respect to 
         "~exists s, t, u ((s  t & s  u) & 
                           ~exists v (t = v & u * v))"

    WN   (weak) normalization
         "~exists s ~exists t (s ->! t)"

    UN   unique normal forms
         "~exists s, t, u (t <-! s ->! u & ~t = u)"

    UN()
         unique normal forms with respect to 
         "~exists s, t, u ((s ! t & s ! u) & ~t = u)"

    UNC  unique normal forms with respect to conversion
         "~exists s, t (((s <->* t & NF(s)) & NF(t)) & ~s = t)"

    NFP  normal form property
         "~exists s, t, u (t <- s ->! u & ~t ->! u)"

    SN   termination (strong normalization)
         "forall t Fin(->*,t) & ~exists u (u ->+ u)"

    diamond
         the diamond property
         "~exists s, t, u (t <- s -> u & ~exists v (t -> v <- u))"

    diamond()
         the diamond property with respect to 
         "~exists s, t, u ((s  t & s  u) & 
                           ~exists v (t  v & u  v))"

    For CR, WCR, SCR, SCR(), UN, UN(), UNC, NFP, diamond 
    and diamond(), there are also ground variants, denoted by a 
    preceding "G".

    CR()
          is confluent
         "~exists t, u (t <-  ->* u & ~t join u)"

    WCR()
    SCR()
    SCR(, )
    WN() 
    UN()
    UN(, )
    NFP()
    diamond()
    diamond(, )
        modifying WCR, SCR, SCR(), WN, UN, UN(), NFP, 
        diamond and diamond() accordingly

    SN() 
         is terminating
        "Fin(->+, ) & ~exists u( ->* u ->+ u)"

    NF()
          is a normal form

    Fin(, )
         finiteness of the set of terms u such that the pair (,u)
         belongs to the binary relation 

Nach oben scrollen