Propositional Logic Flashcards
What is a structured representation?
World model that describes the world using variables while capturing the following:
1. Knowledge: constraints on variables
2. Reasoning: Inference engines to derive knowledge from percepts.
What is a clause?
Proposition of the form:
(h1 or h2 or … or hm) <– (l1 ^ l2 ^ … ^ lk)
What is a propositional knowledge base?
A set of clauses
What is a logical consequence?
A proposition g is called a logical consequence of a knowledge base written as KG |= g
What is an inference engine?
An inference engine decides for any KB, a set of percept atoms and propositions, whether
KB U percepts |= g
The proposition g is called a query
What is a definite clause?
A definite clause is of the form
H <– (A1 ^ … ^ Am)^a
where m > 0, H and every Ai is an atom.
A definite clause KB is a KB that contains only definite clauses
The definite clause inference engine would need to ahndle queries of the form: ask b
How to implement a definite clause inference engine?
An inference engine produces a proof
The algorithm that generates a proof is called a proof procedure
A proof procedure is sound if every proposition g that is derives from S is a logical consequence
A proof procedure is complete if there is a proof of each logical consequences.
How does forward chaining work?
Start from clauses KB U Percepts and generate new logical consequences. Each derivation is built on the clauses in KB U Percepts or the clauses that have already been generated. Use a rule of derivation for inference.
Forward chaining applies Modus Ponens iteratively to the current knowledge to generate new clauses which are then added to the KB.
What is Modus Ponens?
The inference rule
What is Selective Linear Definite Clause (SLD) Resolution?
Start from the query and treat it as a goal.
Infer backward from the goal, each step derives a clause. Answer true and only true if yes is derived.
What are the properties of SLD Resolution?
SLD can be implemented using a search algorithm. If a search procedure has derived the goal, the rules used can be used by forward chaining to infer the query.
IF forward chaining can derive an atom, then the rules can be used to construct an SLD derivation.
What is truth table for -> symbol?
A B A->B
0 0 1
0 1 0
1 0 1
1 1 1
What is truth table for <- symbol?
A B A<-B
0 0 1
0 1 1
1 0 0
1 1 1
What is truth table for<-> symbol?
A B A<->B
0 0 1
0 1 0
1 0 0
1 1 1
