With the following problem: <div class="snippet-clipboard-content notranslate posi

$ metis --version metis 2.3.1 (release 20161108) <p

Simplify outputs $false, maybe wrongly. about metis HOT 3 CLOSED

gilith commented on June 2, 2024

Simplify outputs $false, maybe wrongly.

from metis.

Comments (3)

asr commented on June 2, 2024

$ metis --version
metis 2.3.1 (release 20161108)

2.3.1? I got 2.3.

from metis.

gilith commented on June 2, 2024

Thank you for reporting this: the root-cause was a bug in the printing of the proof, specifically in the conversion of Xor sets to Iff lists. I've pushed and released a fixed version of Metis, and now the output looks like this:

$ metis --version
metis 2.3 (release 20170315)
$ metis --show proof problem.tptp
...
fof(normalize_2_0, plain, (~ p & (~ q <=> ~ r) & (~ p <=> (~ q <=> r))),
    inference(canonicalize, [], [negate_2_0])).

fof(normalize_2_1, plain, (~ p <=> (~ q <=> r)),
    inference(conjunct, [], [normalize_2_0])).

fof(normalize_2_2, plain, (~ q <=> ~ r),
    inference(conjunct, [], [normalize_2_0])).

fof(normalize_2_3, plain, (~ p), inference(conjunct, [], [normalize_2_0])).

fof(normalize_2_4, plain, ($false),
    inference(simplify, [],
              [normalize_2_1, normalize_2_2, normalize_2_3])).
...

Now it's clear how Metis derived $false in this subgoal.

Cheers,

Joe

from metis.