Willem F Esterhuyse Posted January 8, 2023 Share 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? Link to comment Share on other sites More sharing options...
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