search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
290 stars 50 forks source link

Incorrect saturations for problems containing FOOL #454

Open ibnyusuf opened 1 year ago

ibnyusuf commented 1 year ago

Under certain circumstances, we incorrectly claim saturations for FOOL problems.

This happens when we use a preprocessing technique that gets rid of equalities such as inequality splitting or equality proxy. When setting up the saturation algorithm, we do not add superposition, as the problem no longer contains equalities. However, FOOLParamodulation can reintroduce equalities into the problem. Without superposition (and related rules) to deal with these equalities we can then saturate incorrectly.

easychair commented 1 year ago

What is a FOOL problem?

As a side note, inequality splitting preserves satisfiability. Equality proxy can turn an unsatisfiable problem into a satisfiable one.

Andrei

On Wed, 14 Jun 2023 at 12:17, ibnyusuf @.***> wrote:

Under certain circumstances, we incorrectly claim saturations for FOOL problems.

This happens when we use a preprocessing technique that gets rid of equalities such as inequality splitting or equality proxy. When setting up the saturation algorithm, we do not add superposition, as the problem no longer contains equalities. However, FOOLParamodulation can reintroduce equalities into the problem. Without superposition (and related rules) to deal with these equalities we can then saturate incorrectly.

— Reply to this email directly, view it on GitHub https://github.com/vprover/vampire/issues/454, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABVY4BIOGBGYFYHH75YO5S3XLGMWJANCNFSM6AAAAAAZGGOCAI . You are receiving this because you are subscribed to this thread.Message ID: @.***>

ibnyusuf commented 1 year ago

A problem containing terms of interpreted Boolean sort.

Right, so we don't need to worry about equlity proxy in that case since we can't saturate. Only inequality splitting.

@quickbeam123, this seems to be pretty much a corner case. Perhaps the solution that we implemented on the HOL branch will be suitable for master as well.

quickbeam123 commented 1 year ago

I think, this still stays relevant with ep=RSTC. But yes, the fix from the HOL branch could be tried. It seems we are talking of a very cornerny corner case.

easychair commented 1 year ago

Yes, ep=RSTC preserves completeness, but it is hardly useful for anything.

A

On Sat, 17 Jun 2023 at 07:10, Martin Suda @.***> wrote:

I think, this still stays relevant with ep=RSTC. But yes, the fix from the HOL branch could be tried. It seems we are talking of a very cornerny corner case.

— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you commented.Message ID: @.***>