Hardkeis PDF

1. What is the significance of converting sentences to clausal form in automated reasoning? A) It simplifies the resolution process. B) It allows the use of first-order unification. C) It reduces the need for Skolem functions. D) It eliminates the need for...

1. What is the significance of converting sentences to clausal form in automated reasoning? A) It simplifies the resolution process. B) It allows the use of first-order unification. C) It reduces the need for Skolem functions. D) It eliminates the need for Herbrand's theorem. Correct Answer: A) It simplifies the resolution process. 2. In the context of first-order logic, what is meant by the term "most general unifier" (MGU)? Options: 1. A substitution that resolves all literals in a clause. 2. The substitution that results in the most specific instance of a term. 3. The substitution that, when applied, makes two terms identical and is as general as possible. 4. A unifier that only applies to constants. Answer: 3) The substitution that, when applied, makes two terms identical and is as general as possible. 3. In the context of SAT solvers, what is the main role of the DPLL algorithm? Options: 1) To convert formulas into Prenex normal form. 2) To repeatedly apply the resolution rule until a contradiction is found. 3) To systematically search for a satisfying assignment using backtracking and unit propagation. 4) To generate Skolem functions for eliminating existential quantifiers. Answer: 3) To systematically search for a satisfying assignment using backtracking and unit propagation. 4. What is the result of applying resolution to a pair of clauses? A) A single clause B) A contradiction C) A new clause that resolves the original pair D) A truth table Correct Answer: C) A new clause that resolves the original pair 5. How does the Herbrand base differ from the Herbrand universe? A) The Herbrand base includes ground instances of predicates, while the Herbrand universe includes ground terms.  B) The Herbrand base consists of only constants, while the Herbrand universe includes variables. C) The Herbrand base is finite, while the Herbrand universe is infinite. D) The Herbrand base applies only to propositional logic, while the Herbrand universe applies to first-order logic. Correct Answer: A) The Herbrand base includes ground instances of predicates, while the Herbrand universe includes ground terms. 6. Which of the following statements about the completeness of the resolution method is correct? A) Resolution is complete for propositional logic but incomplete for first-order logic. B) Resolution is incomplete for both propositional logic and first-order logic. C) Resolution is complete for both propositional and first-order logic. D) Resolution is complete only when the Skolemization process is applied. Correct Answer: C) Resolution is complete for both propositional and first-order logic. 7. Which of the following is NOT a component of the Skolem normal form? A) Conjunction of clauses B) No existential quantifiers C) Only universal quantifiers at the beginning D) Introduction of Herbrand constants Correct Answer: D) Introduction of Herbrand constants 8. What is the role of unification in first-order logic resolution? A) To eliminate existential quantifiers B) To combine similar terms within clauses C) To match literals and make them identical D) To convert formulas into clausal form Correct Answer: C) To match literals and make them identical 9. Which of the following statements is true about the Skolemization technique in predicate logic? Options: 1) It replaces existential quantifiers with universal quantifiers. 2) It converts formulas into Prenex normal form. 3) It eliminates existential quantifiers by introducing Skolem functions. 4) It is used to simplify Boolean formulas. Answer: 3) It eliminates existential quantifiers by introducing Skolem functions.  10. What does Herbrand's theorem state for a set of first-order logic sentences? Options: 1) Any set of sentences in first-order logic is satisfiable. 2) The satisfiability of a set of first-order sentences can be reduced to the satisfiability of propositional sentences derived from its Herbrand expansion. 3) Every satisfiable formula in first-order logic has a finitely satisfiable subset. 4) A formula in first-order logic is true if and only if it satisfies all interpretations. Answer: 2) The satisfiability of a set of first-order sentences can be reduced to the satisfiability of propositional sentences derived from its Herbrand expansion.