Willem F Esterhuyse Posted January 8, 2023 Posted January 8, 2023 A text says that to prove a formula A we have to refute GA (which must reduce to the negation of A). It says that for each sub-formula of the form B OR C to include the following clauses in GA: {xB OR C, ~xB}, {xB OR C, ~xC}, {xB, xC, ~xB OR C}. Shouldn't there be two ~xB OR C's and one xB OR C? As stated it resolves to xB OR C and not it's negation. If not, why not?
Recommended Posts
Create an account or sign in to comment
You need to be a member in order to leave a comment
Create an account
Sign up for a new account in our community. It's easy!
Register a new accountSign in
Already have an account? Sign in here.
Sign In Now