-
Notifications
You must be signed in to change notification settings - Fork 20
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Tool doesn't find proof [Pairing implies Singleton] #23
Comments
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. |
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: ***@***.***>
|
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. |
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: ***@***.***>
|
When checking for redundant alternatives among prover.alternatives, I used to compare different trees by checking if each open branch on one extends some open branch on another. This is problematic if the trees contain a disjunction p v p (with the same disjunct on both sides). Any branch that develops the left disjunct on tree1 then extends the undeveloped right-hand branch on tree2, even if tree1 and tree2 otherwise explore very different strategies. The present change helps with issue #23 on github, but it causes a regression for Pelletier's problem 51, which was previously provable in 2508 steps and now appears to become unprovable in any reasonable time. (Problems 49 and 52 also perform much worse.)
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.) |
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: ***@***.***>
|
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. |
Interesting. Its nice that it can now automatically find a proof:
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
I speculate a proof without equality is also possible. You
https://www.umsu.de/trees/#~6a~6b~7c~6d%28Edc~4%28Ida~2Idb%29%29~5~6b~7c~6d%28Edc~4Idb%29 The |
Right. The prover finds the tableau with equality first because the other one actually has a larger free-variable tableau. |
My point, that I wanted to make, was the converse.
Or how do you count? But the visible count might be |
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.) |
Strange, this here terminates quickly:
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:
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?
The text was updated successfully, but these errors were encountered: