cl-banner

FORT 2.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(s)
specified in . The syntax of TRSs follows the standard TPDB format.
If the formula uses indexing, several TRSs can be specified below each
other, which are then indexed internally starting from 0.

As optional  the user may specify the number of files that
are given in consecutive files (each containing a single TRS) using -m ,
where  has to be a natural number greater than 0.

The verbosity level can be specified 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).

Witness generation can be enabled with -w.

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 
    -g 
    -v 
    -r " - "
    -s 
    -d 
    -fs
    -opt

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. Alternatively, a signature generator can be
specified using the -g option. This is done via a sequence of arities with
optional surrounding parentheses and '*' to get infinite signatures by
repeating the given pattern. For example (0 0 1 2) corresponds to a
signature containing two constants, one unary and one binary function
symbol, whereas (0 1)* corresponds to an infinite signature with
alternating pattern of a constant and a unary function symbol. If no
signature or signature generator is given, FORT will incrementally
increase the signature starting from a single constant.

The other optional parameters are the maximum number  of differen
variables, the minimum and the maximum number of rewrite rules  and
, and the maximum size  and depth  of terms in the rewrite rules.

If -fs is used, the signature will not be increased incrementally, but the
full signature will be used directly. Furthermore, -opt can be used
to indicate that the smallest TRS in the induced order is returned
instead of the first one found. This brings back determinism also for
the parallel versions of FORT.

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 )
    (SIG_GEN )
    (VARIABLES )
    (RULES " - ")
    (SIZE )
    (DEPTH )
    (FIXED_SIG)
    (OPT)

corresponding to the optional parameters described above.

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

SYNTAX OF FORMULAS

The syntax for  is given by the following EBNF:

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

Here  denotes a natural number, and  any nonempty sequence of
alphanumeric symbols.  and  are comma separated lists 
of s or s, respectively. Moreover,  is a space 
separated list of s. If the formula is not closed, witnesses are 
generated.

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

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
    [, ..., ]  denoted that the formula following it has 
             to hold for the union of the TRSs with specified indices
             (if no index is specified, the union of all TRSs is taken)

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

    '->'       one-step rewriting
    '->='      one or zero steps
    '->+'      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
    '->e+'     transitive closure of '->e'
    '->be+'    transitive closure of '->be'
    '->e*'     transitive reflexive closure of '->e'
    '->be*'    transitive reflexive closure of '->be'
    '<->'      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))"
    
    Com(, )
         commutation of the union of TRSs specified by the first list of 
         indices with the ones specified by the second list of indices.
         Assume we have lists "0 1" and "1 2":
         "~exists s, t, u (([0,1]s ->* t & [1,2]s ->* u) & 
                           ~exists v ([1,2]t ->* v & [0,1]u ->* v))"
    
    LCom(, )
         commutation of the union of TRSs specified by the first list of 
         indices with the ones specified by the second list of indices.
         Assume we have lists "0 1" and "1 2":
         "~exists s, t, u (([0,1]s -> t & [1,2]s -> u) & 
                           ~exists v ([1,2]t ->* v & [0,1]u ->* v))"
         
    For CR, WCR, SCR, SCR(), UN, UN(), UNC, NFP, diamond, 
    diamond(), Com and LCom 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