--------------------------------------------------------------------------- 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