CTRS Format

The format for first-order conditional rewrite systems is a simplification of the old TPDB format, according to the following grammar:

  ctrs     ::= (CONDITIONTYPE ctype) [(VAR idlist)] (RULES rulelist) [(COMMENT string)]
  ctype    ::= SEMI-EQUATIONAL | JOIN | ORIENTED
  idlist   ::= ε | id idlist
  rulelist ::= ε | rule rulelist
  rule     ::= term -> term | term -> term | condlist
  condlist ::= cond | cond, condlist
  cond     ::= term == term
  term     ::= id | id() | id(termlist)
  termlist ::= term | term, termlist

The restrictions on id on string are the same as in the TRS format.

Example

 (CONDITIONTYPE ORIENTED)
 (VAR x)
 (RULES
  not(x) -> false | x == true
  not(x) -> true  | x == false
 )

Converter

Thomas Sternagel provided a converter ctrs-converter.jar between the 'old' TRS format and the modified TRS format. It is a simple command line tool that either accepts the path to a trs file as its sole argument or (if no argument is provided) reads from standard input. The tool outputs the converted CTRS on standard output. It is able to convert in both directions (depending on the format of the input). If the input is in the 'old' format and the tool encounters mixed conditions it issues an error message.