search

wo / tpg

Tree Proof Generator
GNU General Public License v3.0
151 stars 20 forks source link

Valid formula for which the proof can't be constructed due to `TypeError` #14

Closed simonaslaurinavicius closed 2 years ago

simonaslaurinavicius commented 2 years ago

Dear, Wolfgang,

wanted to share with you a valid formula example that raises a TypeError when trying to build a proof for it.

The formula can be accessed here)~1~7x(Ox~1Mx))~1(~6x((Ox~1Mx)~5(~9(Ox~1Sx)~1~9(Ox~1~3Sx)))~1~7x(Ox~1Mx)))~5(~7x(~9(Ox~1Sx)~1~9(Ox~1~3Px))~2~3~7x~9(Ox~1Sx))||universality).

In case something doesn't work (?), formula in prover syntax: ((∀x((Ox∧Mx)→(◇(Ox∧Px)∧◇(Ox∧¬Px)))∧∃x(Ox∧Mx))∧(∀x((Ox∧Mx)→(◇(Ox∧Sx)∧◇(Ox∧¬Sx)))∧∃x(Ox∧Mx)))→(∃x(◇(Ox∧Sx)∧◇(Ox∧¬Px))∨¬∃x◇(Ox∧Sx))

The accessibility relation is universal.

TypeError occurs here, but I'm sure you will get more information by checking the Javascript console after running the formula.

I'm deeply grateful for your work, it's an amazing tool, thank you!

wo commented 2 years ago

Thanks! Good catch. I have barely tested the prover with quantified modal formulas. This should be fixed now on umsu.de. (Currently can't update github.)