proof checking bug

[easychair]

Try this:

vampire --decode lrs+10_1024_to=kbo:proof_extra=full:norm_ineq=on:sas=z3:si=on:sos=on:tha=off:nm=16_10 --proof smtcheck ~/TPTP-v9.1.0/Problems/SWW/SWW617_2.p | grep -v ^% | z3 /dev/stdin

You will see this error:

(error "line 2498 column 63: unknown constant _t2tb (Int) declared: (declare-fun _t2tb (_map_int_int) _uni) ") (error "line 2499 column 68: unknown constant _t2tb (Int) declared: (declare-fun _t2tb (_map_int_int) _uni) ")

[MichaelRawson]

Ugh, I know what this is. At some point between Ground Truth and today, the default for the literal maximality aftercheck turned from off to on - this makes the computed substitution slightly different, which breaks the approach. Set lma=off and this goes through.

I could fix this by re-computing the subsitution in the same way that BinaryResolution et al do it, but I'd need to re-test it on the whole TPTP (and possibly SMT-LIB too) to make sure I didn't break it even more severely. Suggestion for now: set lma=off and cross your fingers, or check out a commit of Vampire from shortly after #695.

There's probably a discussion to be had about what to do about this kind of thing. I don't think we want this kind of maintenance hazard, but it's not clear to me what a better alternative is. I'm working on some Prolog script to do this kind of thing post-hoc, outside of Vampire. If it's easy enough and works well that might be the way forward.

[MichaelRawson]

Also to note that we only tested Ground Truth in default mode on TPTP. Other strategies might work.

[easychair]

I'd suggest that we carefully work on ALL inferences to provide trusted proofs - those that can be checked by SMT solvers plus a small number of other trusted steps. A

…

On Tue, 23 Sept 2025 at 16:51, Michael Rawson ***@***.***> wrote: *MichaelRawson* left a comment (vprover/vampire#764) <#764 (comment)> Also to note that we only tested *Ground Truth* in default mode on TPTP. Other strategies *might* work. — Reply to this email directly, view it on GitHub <#764 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABVY4BKHZZMP6JT3R43KSLL3UFF5DAVCNFSM6AAAAACHIUGQDSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZTGMRUGEYTEOBQHA> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[mezpusz]

This topic is coming up again due to Vampire+Lean. Has anyone tried storing the mapping of the unifier itself in the proof extra, instead of a recipe how to recompute the unifier? We could just store an array of terms t0,t1,...,tn that correspond to x0\theta,x1\theta,...,xn\theta (with possibly empty terms in between).

[MichaelRawson]

You can do this, but it has some (more) overhead. You probably need at least two arrays (RobSubst's left/right banks) and either the output bank as well or some work upfront to store the right terms.

The way I think you want to do this is completely outside of Vampire, or alternatively inside Vampire but at proof reconstruction time (i.e. completely re-perform an inference looking for the clause you know is derivable). proof_extra is probably a misstep and should die (except we now use it for something in synthesis??).