Expanding simplify inference

[jonaprieto]

Hi Joe,

With this problem:

$ cat impl-9.tptp
fof(a1, axiom, ((p => p) => q)).
fof(goal, conjecture, ((q => r) => r)).

I am getting this:

$ metis --show proof impl-9.tptp
fof(a1, axiom, ((p => p) => q)).
fof(goal, conjecture, ((q => r) => r)).
... 
fof(normalize_0_0, plain, (~ r & (~ q | r)),
    inference(canonicalize, [], [negate_0_0])).
fof(normalize_0_1, plain, (q), inference(canonicalize, [], [a1])).
fof(normalize_0_2, plain, ($false),
    inference(simplify, [], [normalize_0_0, normalize_0_1])).
...

The last result ($false) is clear but it expected based on other proofs
something else. What about printing proofs by expanding the simplify step,
like this example:

fof(a1, axiom, ((p => p) => q)).
fof(goal, conjecture, ((q => r) => r)).
... 
fof(normalize_0_0, plain, (~ r & (~ q | r)),
    inference(canonicalize, [], [negate_0_0])).
fof(normalize_0_1, plain, (~ q | r),
   inference(conjunct, [], normalize_0_0)).
fof(normalize_0_2, plain, (q), 
  inference(canonicalize, [], [a1])).
fof(normalize_0_3, plain, (r),
    inference(resolve, [$cnf(q)], [normalize_0_2, normalize_0_1])). 
fof(normalize_0_4, plain, ($false),
   inference(simplify, [], [normalize_0_3, normalize_0_0])).
...

Do we have any chance to expand the simplify inference?

Thanks,

CC'ing @asr

[gilith]

Hi Jonathan,

I agree that there could be a lot happening inside a single "simplify" inference. Unfortunately, I've just taken a look at the relevant code and I think it would take a major redesign to emit finer-grained proof steps, which I don't have the bandwidth to undertake for the foreseeable future.

In case it helps, here is what Metis is doing during this specific "simplify" inference:

1. The formula normalize_0_0 is traversed, and the subformula ~q is replaced with $false using normalize_0_3.

2. When reassembling normalize_0_0 the built-in simplification rules $false | r = r and ~r & r = $false are applied, resulting in what you see in normalize_0_4.

If you needed to implement this functionality for your project I'd be happy to receive a pull-request from you :-)