In this document the usage of FORT is described. If you are Windows user,
replace every occurrence of "./fort" by "fort.exe". Type

    ./fort -h

for a shorter version of this document.

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

VERSION

Type

    ./fort -v

to get the version of FORT.

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

DECISION TOOL

In order to use FORT as a decision tool type

    ./fort -D <file> [<verbosity>] "<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. 
The optional <verbosity> parameter takes a value in { 0, 1, 2 }. The higher
the number the more detailed the output will be. The default value is 0. 
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

    ./fort -S [options] "<formula>"

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

    -f <F>
    -v <V>
    -r <R>
    -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 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 maximum number <R> of rewrite rules, and the maximum size
<S> and depth <D> of terms in the rewrite rules. The default values are
<V> = 1, <R> = 3, <S> = 4, and <D> = 3.

The second way to call the synthesis tool

    ./fort -S [options] <file>

requires a <file> containing a line

    (FORMULA <formula>)

and optional lines

    (FUN <F>)
    (VARIABLES <V>)
    (RULES <R>)
    (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> denotes any nonempty sequence of alphanumeric symbols that does
not start with a number, except the ones already used in the EBNF. Symbols
like '_', '+', '-', '*', '/' and some others are allowed as well. 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 
parentheses used for quantifiers may be omitted. Then quantification binds 
stronger than '&'. 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 ((s -> t & s ->* u) & ~exists v (t ->* v & u ->* v))"

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

    SCR  strong confluence
         "~exists s, t, u ((s -> 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 ((s ->! 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 ((s -> t & s ->! u) & ~t ->! u)"

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

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

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

    SN(<var>) 
        <var> is terminating
        "Fin(->+, <var>) & ~exists u (<var> ->* u & 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>

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

To improve the performance of FORT, it is recommend to set certain OCAML
runtime options:

    export OCAMLRUNPARAM="s=16M,i=64M,o=150"