% Otter simulator for tm % by Robert Keller % % This example includes the encoding of clauses such that an % initial configuration, encoded as a clause, and % containing a string in {a, b, c}* is a theorem % iff the string is of the form a^n b^n c^n for some n. % % However the construction is perfectly general. It shows that % the issue of determining whether a clause is a theorem in % first order logic with a few constant symbols and unary function % symbols, is undecidable. % % In short, first-order predicate calculus is undecidable. % set(auto). list(usable). % TM state: s(L, C, R): s(Left, Control, Right) where Right includes head % Rules Form % q r w q' R: move(s(x, q, r(y)), s(w(x), q', y)) % q r w q' L: move(s(u(x), q, r(y)), s(x, q', u(w(y)))). For each u % q r w q' N: move(s(x, q, r(y)), s(x, q', w(y))). % f("q0", " ") => ["qa", " ", "R"]; move(s((x), qA, B(y)), s(x, ha, B(y))). move(s((x), qR, B(y)), s(x, hr, B(y))). move(s(B(x), qA, X(y)), s(x, qA, B(X(y)))). move(s(B(x), qL, X(y)), s(x, qL, B(X(y)))). move(s(B(x), qL, a(y)), s(x, qL, B(a(y)))). move(s(B(x), qL, b(y)), s(x, qL, B(b(y)))). move(s(B(x), qL, c(y)), s(x, qL, B(c(y)))). move(s(B(x), qR, X(y)), s(x, qR, B(X(y)))). move(s(B(x), qR, a(y)), s(x, qR, B(a(y)))). move(s(B(x), qR, b(y)), s(x, qR, B(b(y)))). move(s(B(x), qR, c(y)), s(x, qR, B(c(y)))). move(s(B(x), qa, B(y)), s(x, qA, B(B(y)))). move(s(B(x), qa, b(y)), s(x, qR, B(b(y)))). move(s(B(x), qa, c(y)), s(x, qR, B(c(y)))). move(s(B(x), qb, B(y)), s(x, qR, B(B(y)))). move(s(B(x), qb, c(y)), s(x, qR, B(c(y)))). move(s(B(x), qc, B(y)), s(x, qR, B(B(y)))). move(s(B(x), qc, a(y)), s(x, qR, B(c(y)))). move(s(B(x), qc, c(y)), s(x, qL, B(X(y)))). move(s(X(x), qA, X(y)), s(x, qA, X(X(y)))). move(s(X(x), qL, X(y)), s(x, qL, X(X(y)))). move(s(X(x), qL, a(y)), s(x, qL, X(a(y)))). move(s(X(x), qL, b(y)), s(x, qL, X(b(y)))). move(s(X(x), qL, c(y)), s(x, qL, X(c(y)))). move(s(X(x), qR, X(y)), s(x, qR, X(X(y)))). move(s(X(x), qR, a(y)), s(x, qR, X(a(y)))). move(s(X(x), qR, b(y)), s(x, qR, X(b(y)))). move(s(X(x), qR, c(y)), s(x, qR, X(c(y)))). move(s(X(x), qa, B(y)), s(x, qA, X(B(y)))). move(s(X(x), qa, b(y)), s(x, qR, X(b(y)))). move(s(X(x), qa, c(y)), s(x, qR, X(c(y)))). move(s(X(x), qb, B(y)), s(x, qR, X(B(y)))). move(s(X(x), qb, c(y)), s(x, qR, X(c(y)))). move(s(X(x), qc, B(y)), s(x, qR, X(B(y)))). move(s(X(x), qc, a(y)), s(x, qR, X(c(y)))). move(s(X(x), qc, c(y)), s(x, qL, X(X(y)))). move(s(a(x), qA, X(y)), s(x, qA, a(X(y)))). move(s(a(x), qL, X(y)), s(x, qL, a(X(y)))). move(s(a(x), qL, a(y)), s(x, qL, a(a(y)))). move(s(a(x), qL, b(y)), s(x, qL, a(b(y)))). move(s(a(x), qL, c(y)), s(x, qL, a(c(y)))). move(s(a(x), qR, X(y)), s(x, qR, a(X(y)))). move(s(a(x), qR, a(y)), s(x, qR, a(a(y)))). move(s(a(x), qR, b(y)), s(x, qR, a(b(y)))). move(s(a(x), qR, c(y)), s(x, qR, a(c(y)))). move(s(a(x), qa, B(y)), s(x, qA, a(B(y)))). move(s(a(x), qa, b(y)), s(x, qR, a(b(y)))). move(s(a(x), qa, c(y)), s(x, qR, a(c(y)))). move(s(a(x), qb, B(y)), s(x, qR, a(B(y)))). move(s(a(x), qb, c(y)), s(x, qR, a(c(y)))). move(s(a(x), qc, B(y)), s(x, qR, a(B(y)))). move(s(a(x), qc, a(y)), s(x, qR, a(c(y)))). move(s(a(x), qc, c(y)), s(x, qL, a(X(y)))). move(s(b(x), qA, X(y)), s(x, qA, b(X(y)))). move(s(b(x), qL, X(y)), s(x, qL, b(X(y)))). move(s(b(x), qL, a(y)), s(x, qL, b(a(y)))). move(s(b(x), qL, b(y)), s(x, qL, b(b(y)))). move(s(b(x), qL, c(y)), s(x, qL, b(c(y)))). move(s(b(x), qR, X(y)), s(x, qR, b(X(y)))). move(s(b(x), qR, a(y)), s(x, qR, b(a(y)))). move(s(b(x), qR, b(y)), s(x, qR, b(b(y)))). move(s(b(x), qR, c(y)), s(x, qR, b(c(y)))). move(s(b(x), qa, B(y)), s(x, qA, b(B(y)))). move(s(b(x), qa, b(y)), s(x, qR, b(b(y)))). move(s(b(x), qa, c(y)), s(x, qR, b(c(y)))). move(s(b(x), qb, B(y)), s(x, qR, b(B(y)))). move(s(b(x), qb, c(y)), s(x, qR, b(c(y)))). move(s(b(x), qc, B(y)), s(x, qR, b(B(y)))). move(s(b(x), qc, a(y)), s(x, qR, b(c(y)))). move(s(b(x), qc, c(y)), s(x, qL, b(X(y)))). move(s(c(x), qA, X(y)), s(x, qA, c(X(y)))). move(s(c(x), qL, X(y)), s(x, qL, c(X(y)))). move(s(c(x), qL, a(y)), s(x, qL, c(a(y)))). move(s(c(x), qL, b(y)), s(x, qL, c(b(y)))). move(s(c(x), qL, c(y)), s(x, qL, c(c(y)))). move(s(c(x), qR, X(y)), s(x, qR, c(X(y)))). move(s(c(x), qR, a(y)), s(x, qR, c(a(y)))). move(s(c(x), qR, b(y)), s(x, qR, c(b(y)))). move(s(c(x), qR, c(y)), s(x, qR, c(c(y)))). move(s(c(x), qa, B(y)), s(x, qA, c(B(y)))). move(s(c(x), qa, b(y)), s(x, qR, c(b(y)))). move(s(c(x), qa, c(y)), s(x, qR, c(c(y)))). move(s(c(x), qb, B(y)), s(x, qR, c(B(y)))). move(s(c(x), qb, c(y)), s(x, qR, c(c(y)))). move(s(c(x), qc, B(y)), s(x, qR, c(B(y)))). move(s(c(x), qc, a(y)), s(x, qR, c(c(y)))). move(s(c(x), qc, c(y)), s(x, qL, c(X(y)))). move(s(x, q0, B(y)), s(B(x), qa, y)). move(s(x, qL, B(y)), s(B(x), qa, y)). move(s(x, qa, X(y)), s(X(x), qa, y)). move(s(x, qa, a(y)), s(X(x), qb, y)). move(s(x, qb, X(y)), s(X(x), qb, y)). move(s(x, qb, a(y)), s(a(x), qb, y)). move(s(x, qb, b(y)), s(X(x), qc, y)). move(s(x, qc, X(y)), s(X(x), qc, y)). move(s(x, qc, b(y)), s(b(x), qc, y)). % f("qa", " ") => ["qA", " ", "L"]; % f("qa", "a") => ["qb", "x", "R"]; % f("qa", "b") => ["qR", "b", "L"]; % f("qa", "c") => ["qR", "c", "L"]; % f("qa", "x") => ["qa", "x", "R"]; % f("qb", " ") => ["qR", " ", "L"]; % f("qb", "a") => ["qb", "a", "R"]; % f("qb", "b") => ["qc", "x", "R"]; % f("qb", "c") => ["qR", "c", "L"]; % f("qb", "x") => ["qb", "x", "R"]; % f("qc", " ") => ["qR", " ", "L"]; % f("qc", "a") => ["qR", "c", "L"]; % f("qc", "b") => ["qc", "b", "R"]; % f("qc", "c") => ["qL", "x", "L"]; % f("qc", "x") => ["qc", "x", "R"]; % f("qA", " ") => ["ha", " ", "N"]; % f("qA", "x") => ["qA", "x", "L"]; % f("qL", " ") => ["qa", " ", "R"]; % f("qL", "a") => ["qL", "a", "L"]; % f("qL", "b") => ["qL", "b", "L"]; % f("qL", "c") => ["qL", "c", "L"]; % f("qL", "x") => ["qL", "x", "L"]; % f("qR", " ") => ["hr", " ", "N"]; % f("qR", "a") => ["qR", "a", "L"]; % f("qR", "b") => ["qR", "b", "L"]; % f("qR", "c") => ["qR", "c", "L"]; % f("qR", "x") => ["qR", "x", "L"]; move(s(x, z, d), s(x, z, B(d))). % more tape on right move(s(d, z, y), s(B(d), z, y)). % more tape on left -reachable(x) | -move(x, y) | reachable(y). % Note that B is the blank, not b. % reachable(s(d, q0, B(a(b(c(B(d))))))). % reachable(s(d, q0, B(a(a(a(b(b(b(c(c(c(B(d))))))))))))). % accept % reachable(s(d, q0, B(a(a(a(b(b(c(c(c(B(d)))))))))))). % reject reachable(s(d, q0, B(a(a(a(a(a(b(b(b(b(b(c(c(c(c(c(B(d))))))))))))))))))). % accept -reachable(s(x, ha, y)) | $answer(accept). -reachable(s(x, hr, y)) | $answer(reject). end_of_list.