The example does not follow the form of logic and resolution in particular. wiki resolution: “produces a new clause implied by two clauses containing complementary literals” e.g. “avb, ~avc => bvc”.
14 Resolve(12,1): 1 and 12 are not of the form avb and do not contain complementary literals. Likewise for 15, 17, 18.
16: 16 is derived from 3 and 15. But if y=x then 15 is true but 16 is false. 16 contradicts 15.
19: 19 (true) is derived from 18 and 16, i.e. x <= y and ~(x <= y). If this is Resolution then we would derive false. Please explain how the expression x<y ? y : x is derived from these two contradictory expressions e.g. if we have x=y and ~(x=y) what expression do we derive? In general, from expressions P and ~P what do we derive?
The reference by Volkstorf is straightforward and contains numerous simple, complete examples. I would suggest that a much better example can be found there.
Welcome to this talk page
Talk pages are where people discuss how to make content on Wikipedia the best that it can be. Use this page to start a discussion about the edits made from this IP address. What you say here will be public for others to see. Many IP addresses change periodically, and are often shared by several people.
This is the discussion page for an IP user, identified by the user's IP address. Many IP addresses change periodically, and are often shared by several users. If you are an IP user, you may create an account or log in to avoid future confusion with other IP users. Registering also hides your IP address. |