AProVE Help: Term Rewrite Systems

Syntax of TRS input files (.trs, .xtrs)

      Program      = { "(" Decl ")" }.
      Decl         = "VAR" {Id} | "THEORY" { "(" ThDecl ")" } | "RULES" {Rule} | "STRATEGY" StrategyDecl | Id [AnyList].
      AnyList      = Any {"," Anylist}.
      Any          = Id | String | "(" AnyList ")".
      ThDecl       = {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))
      )

Syntax of TES input files (*.tes)

      Program    = [VarDecl] [AcDecl] [CDecl] [ADecl] Rule {Rule}.
      VarDecl    = "[" IdList "]".
      AcDecl     = "AC" "[" IdList "]".
      CDecl      = "C" "[" IdList "]".
      ADecl      = "C" "[" IdList "]".
      IdList     = Id { "," Id }.
      Id         = Name | InfixName {InfixName}.
      InfixName  = "@" | "&" | "%" | "/" | "\" | ":" | "-" | "+" | "*" | "." | "<" | ">" | "=" | "!" | "$" | "?" | "^".
      SimpleRule = Term  "->"  Term.
      CondRule   = SimpleRule {"," SimpleRule } "|" SimpleRule.
      Equation   = Term "==" Term.
      Rule       = SimpleRule | CondRule | Equation.
      PrefixTerm = Name | Name "(" Term {"," Term } ")" | "(" Term ")".
      InfixTerm  = PrefixTerm InfixName PefixTerm
      Term       = InfixTerm | PrefixTerm

Name are non-empty sequences of characters except space, '(', ')', '"' and ',' and excluding special sequences '->', '==', '|' and combinations of InfixNames

Examples

Simple Example


      [x,y]
      times(x,plus(y,1)) -> plus(times(x,plus(y,times(1,0))),x)
      times(x,1) -> x
      plus(x,0) -> x
      times(x,0) -> 0

Infix Example


      [x, y, u, v, w]

      (x + y) - y -> x
      0 / (y + 1) -> 0
      (x + 1) / (y + 1) -> ((x - y) / (y + 1)) + 1

      0 + 0 == 0
      1 + 0 == 1
      0 + 1 == 1
      u + (v + w) == (u + v) + w

Conditional Example


      [x, y, x', y', z]
      x -> 0, y -> y' | plus(x, y) -> y'
      x -> s(x'), y -> y' | plus(x, y) -> s(plus(x', y'))
      fibi(0) -> pair(0, s(0))
      fibi(x) -> pair(y, z) | fibi(s(x)) -> pair(z, plus(y, z))
      fib(x) -> sel(fibi(x))
      sel(pair(x, y)) -> x

Syntax of SRS input files (.srs, .xsrs)

      Program      = { "(" Decl ")" }.
      Decl         = "VAR" {Id} | "THEORY" { "(" ThDecl ")" } | "RULES" {Rule} | "STRATEGY" StrategyDecl | Id [AnyList].
      AnyList      = Any {"," Anylist}.
      Any          = Id | String | "(" AnyList ")".
      ThDecl       = {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} ")".

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

Syntax of SES input files (*.ses)

      Program    = [VarDecl] [AcDecl] [CDecl] [ADecl] Rule {Rule}.
      VarDecl    = "[" IdList "]".
      AcDecl     = "AC" "[" IdList "]".
      CDecl      = "C" "[" IdList "]".
      ADecl      = "C" "[" IdList "]".
      IdList     = Id { "," Id }.
      Id         = Name | InfixName {InfixName}.
      InfixName  = "@" | "&" | "%" | "/" | "\" | ":" | "-" | "+" | "*" | "." | "<" | ">" | "=" | "!" | "$" | "?" | "^".
      SimpleRule = Term  "->"  Term.
      CondRule   = SimpleRule {"," SimpleRule } "|" SimpleRule.
      Equation   = Term "==" Term.
      Rule       = SimpleRule | CondRule | Equation.
      PrefixTerm = Name | Name "(" Term {"," Term } ")" | "(" Term ")".
      InfixTerm  = PrefixTerm InfixName PefixTerm
      Term       = InfixTerm | PrefixTerm

Name are non-empty sequences of characters except space, '(', ')', '"' and ',' and excluding special sequences '->', '==', '|' and combinations of InfixNames

Examples

Simple Example


      [x,y]
      times(x,plus(y,1)) -> plus(times(x,plus(y,times(1,0))),x)
      times(x,1) -> x
      plus(x,0) -> x
      times(x,0) -> 0

Infix Example


      [x, y, u, v, w]

      (x + y) - y -> x
      0 / (y + 1) -> 0
      (x + 1) / (y + 1) -> ((x - y) / (y + 1)) + 1

      0 + 0 == 0
      1 + 0 == 1
      0 + 1 == 1
      u + (v + w) == (u + v) + w

Conditional Example


      [x, y, x', y', z]
      x -> 0, y -> y' | plus(x, y) -> y'
      x -> s(x'), y -> y' | plus(x, y) -> s(plus(x', y'))
      fibi(0) -> pair(0, s(0))
      fibi(x) -> pair(y, z) | fibi(s(x)) -> pair(z, plus(y, z))
      fib(x) -> sel(fibi(x))
      sel(pair(x, y)) -> x

AProVE Help: Term Rewrite Systems

Syntax of TRS input files (*.trs, *.xtrs)

Semantical conditions

Examples

Simple Example

Context Sensitive Example

Equational Example

AC Example

Syntax of TES input files (*.tes)

Examples

Simple Example

Infix Example

Conditional Example

Syntax of SRS input files (*.srs, *.xsrs)

Semantical conditions

Examples

Simple Example

Context Sensitive Example

Equational Example

AC Example

Syntax of SES input files (*.ses)

Examples

Simple Example

Infix Example

Conditional Example

Syntax of TRS input files (.trs, .xtrs)

Syntax of SRS input files (.srs, .xsrs)