AProVE Help: Term Rewrite Systems

Syntax of TRS input files (*.trs)

      Program      = { "(" Decl ")" }.
      Decl         = "VAR" {Id} | "THEORY" { "(" ThDecl ")" } | "RULES" {Rule} | "STRATEGY" StrategyDecl | Id [AnyList].
      AnyList      = Any {"," Anylist}.
      Any          = Id | String | "(" AnyList ")".
      ThDecl       = {Id} | "A" {Id} | "C" {Id} | "AC" {Id} | "EQUATIONS" {Equation}.
      Equation     = Term   "=="   Term.
      Rule         = Term  "->"   Term | Term  "->"  Term   "|" CondList.
      CondList     = Cond { "," Cond }.
      Cond         = Term   "->"   Term | Term   "-><-"   Term.
      Term         = Id | Id "(" ")" | Id "(" Termlist ")".
      Termlist     = Term {"," Term}.
      StrategyDecl = INNERMOST | CONTEXTSENSITIVE {Replacements}.
      Replacements = "(" Id  {int} ")".

Id are non-empty sequences of characters except space, '(', ')', '"' and ',' and excluding special sequences '->', '==', '-><-', '|' and keywords CONTEXTSENSITIVE, EQUATIONS, INNERMOST, RULES, STRATEGY, THEORY and VAR.

string are sequences of any characters between double quotes

int are non-empty sequences of digits

Semantical conditions

a symbol declared in a VAR section must not have been used in previous declarations, and is assumed to denote a variable in remaining declarations (in particular must not be applied to arguments)
a symbol occuring in a RULES section which has not been used before is assumed to denote a function symbol, and must be used afterwards always with the same arity.

Examples

Simple Example


      (VAR x y)
      (RULES

        plus(s(s(x)),y) -> s(plus(x,s(y)))
        plus(x,s(s(y))) -> s(plus(s(x),y))
        plus(s(0),y) -> s(y)
        plus(0,y) -> y

        ack(0,y) -> s(y)
        ack(s(x),0) -> ack(x,s(0))
        ack(s(x),s(y)) -> ack(x,plus(y,ack(s(x),y)))
      )

Context Sensitive Example


      (VAR X Y Z)
      (STRATEGY CONTEXTSENSITIVE
        (and 1)
        (true)
        (false)
        (if 1)
        (add 1)
        (0)
        (s)
        (first 1 2)
        (nil)
        (cons)
        (from)
      )
      (RULES
      and(true,X) -> X
      and(false,Y) -> false
      if(true,X,Y) -> X
      if(false,X,Y) -> Y
      add(0,X) -> X
      add(s(X),Y) -> s(add(X,Y))
      first(0,X) -> nil
      first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
      from(X) -> cons(X,from(s(X)))
      )

Equational Example


      (VAR x y u v w)

      (RULES
        minus(plus(x, y), y) -> x
        div(0, plus(y, 1)) -> 0
        div(plus(x, 1),plus(y, 1)) -> plus(div(minus(x, y), plus(y, 1)), 1)
      )
      (THEORY (EQUATIONS
        plus(0, 0) == 0
        plus(1, 0) == 1
        plus(0, 1) == 1
        plus(u, plus(v, w)) == plus(plus(u, v), w)
      ))

AC Example


      (VAR x y)
      (THEORY (AC plus))
      (RULES
        plus(x, 0) -> x
        plus(x, s(y)) -> s(plus(x, y))
      )