Difference between `reflexive, symmetric, transitive` vs `universal` accessibility constraints?

[simonaslaurinavicius]

Hello again, Wolfgang,

I have another question for you.

I'm observing an interesting behavior with some quantified modal logic formulas when using reflexive, symmetric, transitive and universal accessibility constraints.

When using the universal accessibility constraint - formulas are being proved for a really long time (~20k steps), while choosing the reflexive, symmetric, transitive accessibility constraints I'm getting a countermodel almost immediately.

From what I've read, these constraints should be equivalent, right? Or is this not the case for the prover?

Formula examples for the behaviour described above can be found here))~1(~6x(~9(Ox~1Mx)~5(~9(Ox~1Sx)~1~9(Ox~1~3Sx)))~1~9~7x(Ox~1Mx)))~5(~6x(~9(Ox~1Sx)~5~8(Ox~5Px))~1~9~7x(Ox~1Sx))) (((∀x((Ox∧Mx)→¬(◇(Ox∧Px)∧◇(Ox∧¬Px))))∧(∀x(◇(Ox∧Mx)→(◇(Ox∧Sx)∧◇(Ox∧¬Sx)))∧◇∃x(Ox∧Mx)))→(∀x(◇(Ox∧Sx)→□(Ox→Px))∧◇∃x(Ox∧Sx))) and here)~1(~6x(~9(Ox~1Mx)~5~8(Ox~5Sx))~1~9~7x(Ox~1Mx)))~5(~7x((Ox~1Sx)~1~9(Ox~1Px)))) (((∃x(◇(Ox∧Px)∧□(Ox→Mx)))∧(∀x(◇(Ox∧Mx)→□(Ox→Sx))∧◇∃x(Ox∧Mx)))→(∃x((Ox∧Sx)∧◇(Ox∧Px))))

Hope that helps, thanks again!

[wo]

How odd! Thanks. The prover should be faster with the "universal" condition -- although as you say the logic determined by these conditions is the same. I need to investigate what's going on here, Might take a few days since I'm in the middle of moving house.

[wo]

I'm still not entirely sure what's happening here. But I've just committed an update that simplifies the model search, and it seems to resolve the problem. If you still see it with other sentences, do let me know! I'm closing the issue for now.

[simonaslaurinavicius]

Understood, thank you again for a swift response. :) Will keep you posted if I encounter something interesting again.

[simonaslaurinavicius]

@wo not sure whether to open a separate issue, but I completely forgot about another formula I had:

((∀x(◇(Ox∧Mx)→◇(Ox∧Px))∧◇∃x(Ox∧Mx))∧(∀x(◇(Ox∧Sx)→(◇(Ox∧Mx)∧◇(Ox∧¬Mx)))∧◇∃x(Ox∧Sx)))→(∀x(◇(Ox∧Sx)→◇(Ox∧Px))∧◇∃x(Ox∧Sx))

The problem is the opposite and regards the valid formula and it's proof.

With universal constraint~1~9~7x(Ox~1Mx))~1(~6x(~9(Ox~1Sx)~5(~9(Ox~1Mx)~1~9(Ox~1~3Mx)))~1~9~7x(Ox~1Sx)))~5(~6x(~9(Ox~1Sx)~5~9(Ox~1Px))~1~9~7x(Ox~1Sx))||universality) I'm able to find a tree proof in ~3000 steps. With reflexive, symmetric, transitive~1~9~7x(Ox~1Mx))~1(~6x(~9(Ox~1Sx)~5(~9(Ox~1Mx)~1~9(Ox~1~3Mx)))~1~9~7x(Ox~1Sx)))~5(~6x(~9(Ox~1Sx)~5~9(Ox~1Px))~1~9~7x(Ox~1Sx))||reflexivity|symmetry|transitivity) I'm up to 50k steps with no proof..

[wo]

That's what I would have expected. Every frame condition -- reflexive, symmetric, transitive, etc. -- corresponds to a tree rule that is added to the basic rules for K. If you toggle 'universal', the prover switches to simpler and faster proof technique that doesn't keep track of accessibility facts at all. So I don't think this is a bug. If you want a faster proof search, simply use 'universal'.

[simonaslaurinavicius]

Understood, thanks for clarifying that, have a nice rest of the week. :)