Input Format of NaTT
Input method is XML.
sym
::=
a variable or function symbol
<sym>
text
</sym>
term
::=
sym
constant or variable
<app>
sym
function
term
+
arguments
</app>
cond
::=
conditions for conditional rules
<cond>
term
term
</cond>
rule
::=
<rule>
term
left hand side
term
right hand side
cond
*
conditions
</rule>
sym-decl
::=
declares a variable symbol
<var>
text
</var>
declares a function symbol
<fun
theory="
AC?|C
"
>
text
</fun>
Content
<trs>
sym-decl
*
rule
+
(
<infeasibility>
sym-decl
*
cond
+
</infeasibility>
)
?
</trs>