2019-06-25 13:40:40 (GMT)
Hello,
In the TSTP output format and especially in TFF formulas, variables are free (which is not allowed in TPTP syntax), is it a bug that requires a fix or do we need to quantify each variable when we parse a file?
Thanks :)
2019-06-25 13:41:51 (GMT)
I thought variables were indeed quantified in proof steps in TFF, if not that sounds like a bug. Maybe it only quantifies variables of type that is not $i though.
2019-06-25 13:50:30 (GMT)
Do you have a small example showing this behavior?
2019-06-25 14:41:24 (GMT)
I get this on a normal TPTP problem, with proper quantifiers:
% ./zipperposition.exe examples/pelletier_problems/pb61.p -o tstp
% done 1 iterations in 0.013s
% SZS status Theorem for 'examples/pelletier_problems/pb61.p'
% SZS output start Refutation
tff(goal, conjecture, (![X,Y,Z,W]: (f(X,f(Y,f(Z,W))) = f(f(f(X,Y),Z),W)))).
tff(zf_stmt_0, negated_conjecture,
(~(![X,Y,Z,W]: (f(X,f(Y,f(Z,W))) = f(f(f(X,Y),Z),W))))).
tff('0', plain,
f(sk_X, f(sk_Y, f(sk_Z, sk_W))) != f(f(f(sk_X, sk_Y), sk_Z), sk_W),
inference('cnf', [status(esa)], [zf_stmt_0])).
tff(ax1, axiom, (![X,Y,Z]: (f(X,f(Y,Z)) = f(f(X,Y),Z)))).
tff('1', plain, ![X0, X1, X2]: f(X0, f(X1, X2)) = f(f(X0, X1), X2),
inference('cnf', [status(esa)], [ax1])).
tff('2', plain,
f(sk_X, f(sk_Y, f(sk_Z, sk_W))) != f(sk_X, f(sk_Y, f(sk_Z, sk_W))),
inference('demod', [status(thm)], ['0', '1', '1', '1'])).
tff('3', plain, $false, inference('simplify', [status(thm)], ['2'])).
% SZS output end Refutation