Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Why does Vampire give a refutation for axiom “lecturer(fr)” and conjecture “lecturer(fr)”?
Using http://www.tptp.org/cgi-bin/SystemOnTPTP and Vampire there, I am trying out the following:
fof(4, axiom, lecturer(fr)).
fof(query, conjecture, lecturer(fr)).
Why does that find a refutation?
% Refutation found. Thanks to Tanya!
% SZS status Theorem for SOT_z1GY
% SZS output start Proof for SOT_z1GY
fof(f7,plain,(
$false),
inference(subsumption_resolution,[],[f6,f5])).
fof(f5,plain,(
~lecturer(fr)),
inference(cnf_transformation,[],[f4])).
fof(f4,plain,(
~lecturer(fr)),
inference(flattening,[],[f3])).
fof(f3,negated_conjecture,(
~lecturer(fr)),
inference(negated_conjecture,[],[f2])).
fof(f2,conjecture,(
lecturer(fr)),
file('/tmp/RjiEQ76n1Q/SOT_z1GYCV',query)).
fof(f6,plain,(
lecturer(fr)),
inference(cnf_transformation,[],[f1])).
fof(f1,axiom,(
lecturer(fr)),
file('/tmp/RjiEQ76n1Q/SOT_z1GYCV',4)).
% SZS output end Proof for SOT_z1GY
% ------------------------------
% Version: Vampire 4.5.0 (commit 2ee491ce on 2020-06-19 13:55:12 +0100)
% Termination reason: Refutation
On the other hand, Vampire says the following is satisfiable:
fof(4, axiom, lecturer(fr)).
fof(query, conjecture, ~lecturer(fr)).
Vampire negates the conjecture. That’s how classical FOL theorem provers tend to see the world.