search

jkorb / KI1V13001-Inleiding-Logica

This is the source material for the course "Inleiding Logica" (KI1V13001) as taught at Utrecht University for the BSc "Kunstmatige Intelligentie"
Creative Commons Attribution 4.0 International
3 stars 16 forks source link

Identity rule applied to a non atomic formula in the solution to 11.7.1.5 a #116

Open DorusKeijzer opened 3 years ago

DorusKeijzer commented 3 years ago

image

It seems in the solution to 11.7.1.5 a, the tableau rule for identity is used on the negation of an atomic formula (the final step on the rightmost branch), even though strictly the definition of this rule on paragraph 10.3.1 only really specifies that these replacements should be carried out for atomic formulas.

image

and the final lines of 10.3.3 explicitly says that you don't need to do so for negated atomic formulas

image

It would be neater to replace P(p) -> Q(p) with P(c) -> Q(c) and then you can close the tableau for both branches in one step or less per branch without using the identity rule on a negated atomic formula. (The right side will immediately close because of the ¬Q(c) from the initial list and you can close the left side by applying the idenity rule for p = c on P(p))

jkorb commented 2 years ago

Thanks @DorusKeijzer, I'll fix the mistake. I think it's important to keep the rule as is, because otherwise, the required substitutions will explode exponentially...