Final Logic

Question 1

Q1. What is missing from propositional definite clause logic that is present in full propositional logic?

Answer 1

Answer: Propositional definite clause logic misses disjunction and negation of atoms comparing to full propositional logic.

Question 2

Q2. What is the difference between an interpretation and a model in propositional definite clause logic?

Answer 2

Answer: Interpretation maps each proposition to a truth table, all propositions are either true or false, while model is an interpretation where all propositions are true.

Question 3

Q3. Without using the words “model” or “interpretation”, explain what it means to say that

KB |= g.

Answer 3

Answer: It means that whenever all propositions in KB are true, g is also true. (g is logical consequence of KB)

Question 4

Q4. Explain the distinction between syntax and semantics.

Answer 4

Answer: Syntax specifies the symbols used, and how they can be combined to form legal sentences, while semantics specifies the meaning of symbols and sentences.

Question 5

Q5. At its essence, is a proof a syntactic or a semantic operation? why?

Answer 5

Answer: ?

Question 6

Q6. Define what it means for a proof procedure to be complete.

Answer 6

Answer: KB |= g implies that KB |- g. A proof procedure is complete with respect to a semantics if there is a proof of each logical consequence of the knowledge base. Guaranteed to find an answer if it exists.

Question 7

Q7. Define what it means for a proof procedure to be sound.

Answer 7

Answer: KB |- g implies that KB |= g. A proof procedure is sound with respect to semantics of everything that can be derived from a knowledge base is a logical consequence of the knowledge base. Only generates correct answers with respect to semantics.

Question 8

Q8. What does the bottom-up proof procedure for propositional definite clause logic take as input? What does it return as output?

Answer 8

Answer: Bottom-up proof procedure takes a knowledge base and returns set of consequences.

Question 9

Q9. What does it mean to say that the bottom-up proof procedure has reached a fixed point?

Answer 9

Answer: That means that any further application of the rule of derivation does not change the consequence set.

Question 10

Q10. How do we construct the minimal model in the bottom-up proof procedure for definite clause propositional logic? In which sense is it minimal?

Answer 10

Answer: We construct minimal model by setting all atoms in C at the end of BU to true and all other atoms to false. It is minimal in sense that it has the fewest true propositions.

Question 11

Q11. Give a proof procedure that was not presented in the class slides.

Answer 11

Answer: Model elimination proof procedure.

Question 12

Q12. Explain how one step of SLD resolution is performed in the top-down proof procedure.

Answer 12

Answer: In one step of SLD resolution, top-down procedure chooses a definite clause in KB with a(i) as a head and substitutes a(i) with its body in the answer clause. If it can’t find such definite clause the proof procedure fails.

Question 13

Q13. When does the top-down proof procedure terminate?

Answer 13

Answer: Top-down proof procedure terminates when the answer is derived, meaning that the answer clause has empty body, or when the proof procedure fails (can’t find a clause with a(i) as head).

Question 14

Q14. Does it make sense to talk about the truth value of a variable in Datalog? Why or why not?

Answer 14

Answer: Yes, because datalog just extends the propositional definite clause logic. And variables are build on top of atoms.

Question 15

Q15. When does SLD resolution terminate?

Answer 15

Answer: When it can’t find a clause with a(i) as head.

Question 16

Q16. Explain why SLD resolution can result in failing derivations even when the query is entailed by the knowledge base.

Answer 16

Answer: Because in cases when there are several propositions to choose when substituting a proposition, all with same head, wrong choice may lead to failing derivation even though the query is entailed by the knowledge base.

Question 17

Q17. Why might you prefer to use SLD resolution instead of the bottom-up proof procedure?

Answer 17

Answer: SLS resolution would be preferred when we want to prove one or few atoms, as it is proves only atoms that are relevant to the query while bottom-up proves all atoms.

Question 18

Q18. Why might you prefer to use the bottom-up proof procedure instead of SLD resolution?

Answer 18

Answer: Bottom-up proof procedure may be prefered if we want to prove every atom.