User talk:2601:184:4081:1CBE:BCCD:9145:66F5:A63E
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.
 | 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. |