[BUG] Short Truth-Table v Elimination rules checks out when it should not

[Bram28]

Description

Short Truth-Table v Elimination rules checks out when it should not

Steps to Reproduce

Open a puzzle with a green (true) v . Make left or right (or both) side green and justify with v Elimination. That checks out ... but it should not.

Expected Behavior

What should happen is that you get a red transition: not a good inference!

Screenshots

Start:

Make left side green:

Justify with v elim

Oops! Transition is green. Nope, this is not right!

Puzzle Files

STT19OrEliminationBug.zip

Additional Context

Chase says that the v Elim rule at some point calls the v Intro rule!

[N-Desmarais]

Bug Description

When proving an elimination rule the software currently disproves if and only if a contradiction can be found using the corresponding contradiction rule. In this example the corresponding contradiction to Or-Elimination is Or-Contradiction.

This means the transition will only be invalid if the affected cells follow one of these 3 patterns:

In our example the affected cells do not follow any of the above patterns:

This means no Or-Contradiction is found and therefore the software incorrectly accepts the justification for the transition.

How To Correct

This bug is not specific to Or-Elimination it applies to all elimination rules. The issue lies in the fact that not having a corresponding contradiction doesn't imply the justification for the given transition is correct. Another example:

reproduced with bi conditional elim:

In order to resolve this, the process for justifying an elimination rule needs to be completely refactored to follow a logically valid set of steps. This likely means enumerating the patterns that are logically justified and checking against those instead of the corresponding contradiction. Will discuss more with chase about implementation details

[Bram28]

Thanks for looking into this so quickly! If the rule is implemented as you describe, then your analysis is exactly correct: A claim is not forced to have a certain truth-value just because no contradiction is found when it has that truth-value. The latter only means that the claim can possibly have that truth-value ('possible' defined relative to the local context of the applied rule), but that does not make it necessary.

What the implementation should do instead is to check that if we give the claim its opposite truth-value, then we do get a contradiction. So, for example, say you have a false disjunction, and you indicate that this means that the left side is also false. The rule should now consider what happens if that left side is true. And, when it does, it finds a v-Contradiction. So: the claim cannot be true, and is therefore indeed forced to be false. So, we can have these basic rules rely on contradiction rules ... just not how it is currently done!

[GENERAL COMMENT] Note that what I just described here is of course a specific case of the general principle that should work for any LEGUP puzzle: A basic rule that says that some square is forced to be have some content checks out if and only if giving it any of the other possible contents leads to a contradiction ... this is why so many basic rules should be able to be reduced to case and contradiction rules ... and why LEGUP should have this at the core of its engine, i.e. that it is possible to 'implement' basic rules simply by reference to certain case and contradiction rules. I think we have made a start on that, right? Or at least I believe some basic rules are implemented by reference to contradiction rules ... I believe a simple reference to one or more case rules was a little more tricky. Let me also point out that for some puzzles some of the basic rules do currently not reduce to a simple combination of case and contradiction rules as defined ... maybe we should always add case and contradiction rules so that they always can be?

[N-Desmarais]

Submitted a fix that applies the proper negation before checking for contradiction, program shows expected behavior:

Invalid applications of rules no longer creating valid board states:

Getting the correct error message for misuse of a rule:

Valid applications of rules working properly:

Not sure I've seen enough to weigh in on whether or not the case/contradiction rules can be implemented universally. That being said if it was possible this technique would work universally, and any puzzle specific implementations could be trimmed out.