Confluence Competition

CTRS Format

This page explains the format for conditional TRSs.


We use a slightly modified version of the old TPDB format. The modification concerns a new declaration CONDITIONTYPE, which may be set to one of SEMI-EQUATIONAL, JOIN, or ORIENTED. In the conditional part of the rules we only allow == as relation, since the exact interpretation is inferred from the CONDITIONTYPE declaration.

Formally, decl and cond of the grammar of the old TPDB format are replaced as follows:

 decl ::= VAR idlist | RULES listofrules | CONDITIONTYPE condtypedecl | id anylist
 cond ::= term == term 


An example of the format is as follows:

 (VAR x)
  not(x) -> false | x == true
  not(x) -> true  | x == false


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.