gilith/metis

Splitting a goal that look like ~(p <=> q)

jonaprieto opened this issue · 3 comments

jonaprieto commented

Consider this TPTP problem

$ cat issue.tptp 
fof(goal, conjecture, (~ (p <=> q)) <=> ((p => ~ q) & (q => ~p))).

Metis finds a proof when EProver and Vampire don't. (The problem is not a tautology).

$ metis issue.tptp 
SZS status Theorem for issue.tptp

Testing with EProver with a client for SystemOnTPTP (online-atps).

$ online-atps --atp=e issue.tptp                
...
# No proof found!
# SZS status CounterSatisfiable
...

and using Vampire:

$ online-atps --atp=vampire issue.tptp  
...
% Refutation not found, incomplete strategy
% ------------------------------
% Version: Vampire 4.2 (commit c955596 on 2017-07-21 22:07:53 +0100)
...
% SZS status CounterSatisfiable for SOT_wXKR
...

Metis uses this formula (above) to split goal as I found in the source of the split method, and confirmed in the test SPLIT_NOT_IFF.

So, consider this sligthly modification:

$ cat issue.tptp 
fof(goal, conjecture, (~ (p <=> q)) => ((p => ~ q) & (q => ~p))).
$ online-atps --atp=vampire issue.tptp --only-check
Theorem

I hope it be easy to fix.

Thanks in advance,

CC'ing @asr

gilith commented

Hi Jonathan,

Thank you for reporting this soundness bug. Unfortunately your suggested fix doesn't work because Metis uses this splitting rule to reduce a goal of the form ~(X <=> Y), and so I need the implication to be this way around: Z => ~(X <=> Y).

I settled on this solution: ~(p <=> q) <=> ((p => ~q) & (~q => p)) which I believe is valid, and added the old version as a regression test called SPLIT_NOT_IFF_BUG.tptp. I have released the fixed version as Metis 2.3 (release 20170810) and checked it in to this repo as commit b53b0bb

Thanks again,

Joe

jonaprieto commented

Joe,

Thanks for solving this bug. I know that Metis was ported into Isabelle, so I was wondering if this bug is present in the version of Metis that is Isabelle.

Best,

Jonathan.

gilith commented

Hi Jonathan,

As far as I know Metis is only used in Isabelle to prove goals that have already been reduced to CNF, so this soundness bug would not have manifested there. (And, since Isabelle replays Metis proofs, a soundness bug in Metis would never result in a soundness bug in Isabelle, just a proof that failed to replay.)

Cheers,

Joe

  • 👍1