mkbTT

mkbTT online

Input Input can either be supplied in both the old or the new TPDB
format or in TPTP format. Please check
http://www.lri.fr/~marche/tpdb/format.html
http://www.termination-portal.org
http://www.cs.miami.edu/~tptp
for details about the respective format.

Here is an example (CGE2) in TRS format:

(VAR x y z)
(RULES
*(e,x) -> x
*(i(x),x) -> e
*(*(x,y),z) -> *(x,*(y,z))
f(*(x,y)) -> *(f(x),f(y))
g(*(x,y)) -> *(g(x),g(y))
*(f(x),g(y)) -> *(g(y),f(x))
)
(example)  
 
standard completion    ordered completion    normalized completion
Output
completed TRS    statistics    proof
Expert Mode