- Please DO NOT use any AI tools like Chat-GPT to generate codes/answers as that'd a violation.

Note: Here sometimes a subscript is indicated with an underscore, e.g., |=_ . "v.a." will be an abbreviation for "variable assignment"

1.a. (5) Suppose that is "almost" a (forward) proof of , except that has been inserted as an assumption, even though it's neither an instance of a logical axiom of the forward proof system, nor in the set of premises , nor derivable from . Now assume is a correct proof of . Show all the ways in which and can be added to the original formula sequence to produce a forward proof of , in a manner that guarantees that the proof will be correct, no matter what the deduction rules of the assumed proof system happen to be. (This is just a simple test of your understanding of the concept of a (forward) proof.) b. (5) In intuitive terms, why does the *soundness* of a proof system require not only that the deduction rules should be sound, but also that any logical axioms (or schemas) that are part of the proof system should be *valid*? c. (5) Why is refutation completeness all we really need in a complete proof system, assuming that we're allowing proofs by contradiction?

2. (15) Given that Every monkey has a tail Koko does not have a tail give a resolution proof that Koko is not a monkey. Use K for Koko, M(x) for "x is a monkey", T(x) for "x is a tail", and H(x,y) for "x has y (as a part)". Remember: Form the negation of the conclusion and only *then* convert to clause form.

3. Some more practice in formal semantics jargon... a. (5) Simplify as much as possible: T_{IU_x:d}(x), T_{IU_x:d}(f(x)), ((U_x:d)_x:e)(x) (Note that T_{IU_x:d}(x) means applying term assignment T_{IU_x:d} to argument x. Here {IU_x:d} is the subscript of T, and x:d is the subscript of U. Similarly for T_{IU_x:d}(f(x)). ((U_x:d)_x:e) means we first alter v.a. U so that it assigns d as the value of x, and then we alter the resulting v.a. so that it assigns e as the value of x.)

b. (5) Express the following in English, without using the words "valid", "entails" "derives", or "logical consequence"; talk about models, proofs, and theorems instead: |= , |- , |= , |-

4. Convert to clause form, showing successive steps: a. (5) x.Integer(x)=>y.(y=sqrt(x) Integer(y)) b. (5) x.y.z.(x > (y-z))

5. a. (5) Find the most general unifier of the argument lists (f(x),x,g(x)) (f(g(u)),g(f(v)),g(g(f(A))))

b. (5) Find all resolvents of P(A)Q(x,x), P(y)P(B)Q(y,f(y))Q(z,f(B))

c. (5) Find all factors of the second clause in (b) above.

d. (5) Find all paramodulants of the following clauses: f(x)=A P(x), Q(f(A),B) Q(A,B)

6. Given: If one individual bribes another, both are corrupt. Don bribes Earl. Fred is not currupt.

Use Cordell Green's method to answer the question, Who bribes whom else, while not bribing everyone?

Note that the question asks for *two* entities to be determined. Also, strictly speaking the first premise (and perhaps the question as well) involves an equality, but just ignore this aspect!

Use B(x,y) for "x bribes y", C(x) for "x is corrupt", D for "Don", E for "Earl" and F for "Fred". Use no other symbols. a. (10) Start by writing the FOL versions of the premises and the conclusion to be proved (to answer the question), and then showing the clause forms of the premises and denial of the "conclusion". b. (10) Then obtain a refutation (using the notational conventions specified in class), and appropriately apply Green's method to extract an answer from the refutation.

7. Given: Romeo loves only one individual, and she is a Capulet. Whoever loves someone has their love returned. Juliet loves Romeo.

Use resolution and paramodulation, and Green's method, to answer the question "Who is a Capulet?"; the answer should be Skolem-free.

Use L(x,y) for "x loves y", C(x) for "x is a Capulet", R for "Romeo", and J for "Juliet". Use no other predicates besides L, C and equality. a. (10) Start by writing the FOL versions of the premises and the conclusion to be proved (to answer the question), and then showing the clause forms of the premises and denial of the "conclusion". b. (10) Then obtain a refutation (using the notational conventions specified in class), and appropriately apply Green's method to extract an answer from the refutation.

- Please answer all the questions/parts as all are part of one single assignment and I cannot ask them in parts.