Tool doesn't find proof [Pairing implies Singleton]

[Jean-Luc-Picard-2021]

Strange, this here terminates quickly:

∀a∀b∃c∀d(Edc ↔ (d=a ∨ d=b)) → ∀b∃c∀d(Edc ↔ (d=b ∨ d=b)) is valid.

https://www.umsu.de/trees/#~6a~6b~7c~6d(Edc~4(d=a~2d=b))~5~6b~7c~6d(Edc~4(d=b~2d=b))

But this here doesn't terminate:

∀a∀b∃c∀d(Edc↔(d=a∨d=b))→∀b∃c∀d(Edc↔d=b) runs and runs and runs

https://www.umsu.de/trees/#~6a~6b~7c~6d(Edc~4(d=a~2d=b))~5~6b~7c~6d(Edc~4d=b)

Any idea whats going on?

[wo]

Odd! Not sure why this happens. Unfortunately both proofs are quite complex, and they diverge early on. Would (will?) take some time to get to the bottom of this.

[beaubranson]

Sorry if I’m being dumb, but is this really that surprising? I thought anything beyond propositional logic was undecidable, so that (especially when you have some existential and universal quantifiers stacked up like this) any algorithm could potentially get stuck in a loop. I assume you could change the algorithm so it would catch this, but that that would probably make it break down on other formulae.

I seem to remember having had a number of cases where it got stuck on one formula but I found an equivalent formula that it got. So for a presentation / demonstration I just had to pick the version that worked. (I haven’t kept track of any of them, though.)

Am I crazy / dumb, or just missing something?

Beau Branson, Ph.D. Associate Professor of Philosophy Philosophy Area Coordinator Assistant General Education Area Coordinator Chair, Humanities and Fine Arts Division 153 B-T Hall Brescia University 717 Frederica St. Owensboro, KY 42301 On Jul 14, 2023 at 7:24 AM -0500, Wolfgang Schwarz @.***>, wrote:

Odd! Not sure why this happens. Unfortunately both proofs are quite complex, and they diverge early on. Would (will?) take some time to get to the bottom of this. — Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you are subscribed to this thread.Message ID: @.***>

[wo]

The problem is that the equality rules can often be applied in many ways, so I have to explore a lot of alternative tree constructions in parallel until I find one that closes. Without equality, there are fewer alternatives to explore. For some reason, the superfluous disjunction also causes the prover to explores fewer simultaneous alternatives. Not sure why.

If the prover seems stuck, this is practically always because it is considering too many alternatives and keeps adding new ones, so that it makes very slow progress on each of them.

[beaubranson]

Thanks to both of you for the explanations. I somehow wasn’t aware of the decidable / semi-decidable distinction, but this makes sense now.

Beau Branson, Ph.D. Associate Professor of Philosophy Philosophy Area Coordinator Assistant General Education Area Coordinator Chair, Humanities and Fine Arts Division 153 B-T Hall Brescia University 717 Frederica St. Owensboro, KY 42301 On Jul 14, 2023 at 11:23 AM -0500, Wolfgang Schwarz @.***>, wrote:

The problem is that the equality rules can often be applied in many ways, so I have to explore a lot of alternative tree constructions in parallel until I find one that closes. Without equality, there are fewer alternatives to explore. For some reason, the superfluous disjunction also causes the prover to explores fewer simultaneous alternatives. Not sure why. If the prover seems stuck, this is practically always because it is considering too many alternatives and keeps adding new ones, so that it makes very slow progress on each of them. — Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you were mentioned.Message ID: @.***>

[wo]

I've found (and fixed) a problem that seems to have caused this. Unfortunately, the fix slows down some other test cases, especially Pelletier's problem 51%20|=%20%E2%88%83z%E2%88%80x(%E2%88%83w%E2%88%80y(Fxy%20%E2%86%94%20y=w)%20%E2%86%94%20x=z)), which used to take 3 seconds and now takes 30. (You can see how it's exploring way too many alternatives.)

[beaubranson]

When I click the link it only runs for about 3 seconds.

Beau Branson, Ph.D. Associate Professor of Philosophy Philosophy Area Coordinator Assistant General Education Area Coordinator Chair, Humanities and Fine Arts Division 153 B-T Hall Brescia University 717 Frederica St. Owensboro, KY 42301 On Jul 15, 2023 at 9:10 AM -0500, Wolfgang Schwarz @.***>, wrote:

I've found (and fixed) a problem that seems to have caused this. Unfortunately, the fix slows down some other test cases, especially Pelletier's problem 51, which used to take 3 seconds and now takes 30. (You can see how it's exploring way too many alternatives.) — Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you were mentioned.Message ID: @.***>

[wo]

Maybe you still have the old version in cache? Otherwise there's a good chance that your computer is faster than mine. I'm working on an 11 year old thinkpad.

[Jean-Luc-Picard-2021]

Interesting. Its nice that it can now automatically find a proof:

∀a∀b∃c∀d(Edc ↔ (d=a ∨ d=b)) → ∀b∃c∀d(Edc ↔ d=b) is valid.

https://www.umsu.de/trees/#~6a~6b~7c~6d(Edc~4(d=a~2d=b))~5~6b~7c~6d(Edc~4d=b)

But it seems it finds a proof in FOL=. I see the following inference step, which is I guess substitution:

26. ¬Eef(18,17,LL)

I speculate a proof without equality is also possible. You can see a proof shape here:

∀a∀b∃c∀d(Edc ↔ (Ida ∨ Idb)) → ∀b∃c∀d(Edc ↔ Idb) is valid.

https://www.umsu.de/trees/#~6a~6b~7c~6d%28Edc~4%28Ida~2Idb%29%29~5~6b~7c~6d%28Edc~4Idb%29

The FOL only proof is one step shorter and more symmetric. Just some observations, don't worry.

[wo]

Right. The prover finds the tableau with equality first because the other one actually has a larger free-variable tableau.

[Jean-Luc-Picard-2021]

My point, that I wanted to make, was the converse. Its not lager, its smaller, you can check by yourself:

FOL= proof: 28 steps
FOL proof: 27 steps

Or how do you count? But the visible count might be different from some internal counting? And also maybe give a bad indicator how proof search and enumeration is done?

[wo]

Yes, the visible tableaux are quite different from the internal ones. After an internal proof has been found I convert it into the visible proof, removing all unused steps. (There's still room for improvement: one could easily bring the FOL proof down to 26 nodes by moving nodes 24 and 21 onto the tree trunk.)