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

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 [<options_d>] <file> "<formula>"

The <formula> specifies the property that should be tested on the TRS
specified in <file>. The syntax of TRSs follows the standard TPDB format.
As optional <options_d> the user may specify the verbosity level with
-v <v>, where <v> 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 <t>, where the natural number <t> is interpreted as seconds.
The syntax of <formula> 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 [<options_s>] "<formula>"

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

    -f <F>
    -v <V>
    -r "<R1> - <R2>"
    -s <S>
    -d <D>

The signature <F> 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 <V> of different
variables, the minimum and the maximum number of rewrite rules <R1> and
<R2>, and the maximum size <S> and depth <D> of terms in the rewrite rules.
The default values are <V> = 1, <R1> = 0, <R2> = max{R1, 3}, <S> = 4, and
<D> = <S> - 1. You may also specify "<R1> -", "- <R2>", or "<R>" 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 <file>

requires a <file> containing a line

    (FORMULA <formula>)

and optional lines

    (FUN <F>)
    (VARIABLES <V>)
    (RULES "<R1> - <R2>")
    (SIZE <S>)
    (DEPTH <D>)

corresponding to the optional parameters described above.

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

SYNTAX OF FORMULAS

The syntax for <formula> is given by the following EBNF:

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

Here <var> 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(<gtt_rel>)
         strong confluence with respect to <gtt_rel>
         "~exists s, t, u ((s <gtt_rel> t & s <gtt_rel> u) & 
                           ~exists v (t <gtt_rel>= v & u <gtt_rel>* v))"

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

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

    UN(<gtt_rel>)
         unique normal forms with respect to <gtt_rel>
         "~exists s, t, u ((s <gtt_rel>! t & s <gtt_rel>! 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(<formula2>)
         the diamond property with respect to <formula2>
         "~exists s, t, u ((s <formula2> t & s <formula2> u) & 
                           ~exists v (t <formula2> v & u <formula2> v))"
         
    For CR, WCR, SCR, SCR(<gtt_rel>), UN, UN(<gtt_rel>), UNC, NFP, diamond 
    and diamond(<formula2>), there are also ground variants, denoted by a 
    preceding "G".

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

    WCR(<var>)
    SCR(<var>)
    SCR(<gtt_rel>, <var>)
    WN(<var>) 
    UN(<var>)
    UN(<gtt_rel>, <var>)
    NFP(<var>)
    diamond(<var>)
    diamond(<formula2>, <var>)
        modifying WCR, SCR, SCR(<gtt_rel>), WN, UN, UN(<gtt_rel>), NFP, 
        diamond and diamond(<formula2>) accordingly

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

    NF(<var>)
         <var> is a normal form

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