Final Logic Flashcards Preview

CPSC 322: Artificial Intelligence > Final Logic > Flashcards

Flashcards in Final Logic Deck (18)
Loading flashcards...
1
Q

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

A

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

2
Q

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

A

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.

3
Q

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

KB |= g.

A

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

4
Q

Q4. Explain the distinction between syntax and semantics.

A

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.

5
Q

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

A

Answer: ?

6
Q

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

A

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.

7
Q

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

A

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.

8
Q

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

A

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

9
Q

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

A

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

10
Q

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?

A

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.

11
Q

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

A

Answer: Model elimination proof procedure.

12
Q

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

A

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.

13
Q

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

A

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).

14
Q

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

A

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

15
Q

Q15. When does SLD resolution terminate?

A

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

16
Q

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

A

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.

17
Q

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

A

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.

18
Q

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

A

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