Q1. What is missing from propositional definite clause logic that is present in full propositional logic?
Answer: Propositional definite clause logic misses disjunction and negation of atoms comparing to full propositional logic.
Q2. What is the difference between an interpretation and a model in propositional definite clause logic?
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.
Q3. Without using the words “model” or “interpretation”, explain what it means to say that
KB |= g.
Answer: It means that whenever all propositions in KB are true, g is also true. (g is logical consequence of KB)
Q4. Explain the distinction between syntax and semantics.
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.
Q5. At its essence, is a proof a syntactic or a semantic operation? why?
Q6. Define what it means for a proof procedure to be complete.
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.
Q7. Define what it means for a proof procedure to be sound.
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.
Q8. What does the bottom-up proof procedure for propositional definite clause logic take as input? What does it return as output?
Answer: Bottom-up proof procedure takes a knowledge base and returns set of consequences.
Q9. What does it mean to say that the bottom-up proof procedure has reached a fixed point?
Answer: That means that any further application of the rule of derivation does not change the consequence set.
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: 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.
Q11. Give a proof procedure that was not presented in the class slides.
Answer: Model elimination proof procedure.
Q12. Explain how one step of SLD resolution is performed in the top-down proof procedure.
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.
Q13. When does the top-down proof procedure terminate?
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).
Q14. Does it make sense to talk about the truth value of a variable in Datalog? Why or why not?
Answer: Yes, because datalog just extends the propositional definite clause logic. And variables are build on top of atoms.
Q15. When does SLD resolution terminate?
Answer: When it can’t find a clause with a(i) as head.
Q16. Explain why SLD resolution can result in failing derivations even when the query is entailed by the knowledge base.
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.
Q17. Why might you prefer to use SLD resolution instead of the bottom-up proof procedure?
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.
Q18. Why might you prefer to use the bottom-up proof procedure instead of SLD resolution?
Answer: Bottom-up proof procedure may be prefered if we want to prove every atom.