Propositional Logic ​
Semantics ​
The truth value of a sentence is based on the truth value of atoms, and for complex sentences how the truth values are combined.
Basic Example
- p is true.
- q is true.
is true.
Truth tables are used to easily determine the truth values of complex sentences.
Truth Table
p | q | |
---|---|---|
true | true | true |
false | true | false |
true | false | false |
false | false | false |
model
A model in propositional logic is simply ann assignment of truth values for the atoms of a sentence. For example if the set of atoms is {p, q}
, a model might be { p = true, q = true }
. Some models can satisfy the entire proposition others may not. (I remember this as each row in a truth table is a model.)
A model can be thought of as an abstract representation of the state of a real or abstract world.
The model M satisfies
- Notation:
the set of models that satisfy
For example {p: true, q: true}
satisfies
Entailment
For Example:
- $M(KB) =
{(p is true, q is true)}
- $M(\alpha) =
{(p is true, q is true), (p is true, q is false)}
Terminology ​
- Logical Equivalence:
. - Example:
- Example:
- Validity: A sentence
is valid if it is true in all models (tautology) - Example:
- Example:
- Satisfiability: a sentence
is satisfiable if it is true in some model, i.e.
Reasoning ​
Reasoning is the use of propositional logic by the agent to select is actions. The approach to doing this is to model the environment of the agent with a knowledge base. Then inference or reasoning is done on the knowledge base to determine the agent's next action.
info Proving ​
info proving: applying rules to derive a proof of
Example: Modus Ponens:
The main challenge is to find which rule needs to be applied to which formulas in order to arrive at the desired conclusion.
Resolution Rule ​
Eliminate opposite literals of two disjuncts. reminder: disjunction == or.
Simple Resolution Rule:
Example:
Simple Resolution Rule With Disjunction.
Example:
Resolution Rule
Where ik and mj are complementary literals:
basically the literals cancel out in the derived disjunction.
To be able to use the resolution rule we need to write our formulas in CNF (conjunctive normal form). The resolution rule can then be applied to the conjuncts.
Proof by Resolution ​
Goal is to prove
Steps:
- add
to KB and try to prove (proof by contradiction) - Write
in CNF - Apply resolution rule until no new clause can be added anymore or false is derived.
Soundness & Completeness ​
- Logical consequence
: semantic entailment, defined through models : a proof exists showing that by applying syntactic rules, follows from KB.
- It is sound if it is proven by resolution that
follows from KB then - It is complete if
then it can be proven by resolution that follows from KB.