Intro to AI - Knowledge
ai knowledge cs50Definitions
knowledge-based agents | Agents that reason by operating on internal representations of knowledge are called knowledge-based agents, they use a knowledge base as their environment to action upon. |
proposition | A Proposition is a statement that can be true or false . |
compound proposition | Compound propositions are formed by connecting propositions by Logical Connectives. |
atomic proposition | The propositions without logical connectives are called atomic propositions. They can be represented by Symbols like P or Q |
sentence | An assertion about the world in some kind of knowledge representation language is called a sentence. |
knowledge base | A knowledge base is a set of sentences known by a knowledge-based agent. |
propositional logic | Propositional logic deals with propositions and argument flow, it is also called "zeroth-order logic". |
predicate logic | Predicate logic uses quantified variables over non-logical objects and allows the use of sentences that contain quantified variables and relations, it is also known as "first-order logic". |
model | A model is an assignment of a truth value (a state) to every propositional symbol (a "possible world"). |
clause | A clause is a disjunction of literals e.g. \$alpha vee beta vee gamma \$ |
conjunctive normal form (CNF) | The conjunctive normal form is a logical sentence that is a conjunction of clauses e.g. \$ ( alpha vee beta vee gamma ) wedge ( delta vee not epsilon) \$ |
entailment \$alpha |-- beta\$ | In every model in which sentence α is true sentence β is also true. This is also called "syntactic consequence". |
inference | Inference is the process of deriving new sentences from old ones. |
Inference Algorithms | Inference Algorithms try to answer the question "does the Knowledge Base KB entail a certain sentence α " \$KB |-- alpha\$ Some examples of Inference Algorithms are Model Checking and Theorem Proving |
Logical Connectives
negation | \$not\$ | not |
conjunction | \$wedge\$ | and |
disjunction | \$vee\$ | or |
implication | \$rarr\$ | if … then |
equivalence | \$harr\$ | iff, if and only if |
Model Checking
Model Checking is an Inference Algorithms,
to determine if KB ⊨ α:
- Enumerate all possible models.
- If in every model where KB is true, α is true, then KB entails α.
- Otherwise, KB does not entail α.
This approach is very resource intensive since for ever proposition we need to enumerate two states (true and false) and combine with all possible states of the remaining propositions. For n propositions this gives us 2n possible states which must be enumerated.
Inference Rules
To implement a better Inference Algorithm we try to use Inference Rules that can be applied to an existing KB in order to extract more information and hopefully the state of α
Modus Ponens
\$ alpha rarr beta \ , alpha \ \ |-- \ \ beta \$
Modus Ponens is latin for "mode that affirms". The following truth table shows all possible values of the premises \$ alpha rarr beta \$ and \$ alpha \$, they are both true only in the last line. On this line \$ beta \$ is also true. Therefore, whenever \$ alpha rarr beta \$ is true and \$ alpha \$ is true, \$ beta \$ must also be true.
\$ alpha \$ | \$ beta \$ | \$ alpha rarr beta \$ |
false | false | true |
false | true | true |
true | false | false |
true | true | true |
Modus Tollens
\$ alpha rarr beta \ , not beta \ \ |-- \ \ not alpha \$
Transposition
\$ alpha rarr beta \ \ |-- \ \ not beta rarr not alpha \$
And Elimination
\$ alpha wedge beta \ \ |-- \ \ alpha \$
Double Negation Elimination
\$ not(not alpha) \ \ |-- \ \ alpha\$
Implication Elimination
\$ alpha rarr beta \ \ |-- \ \ not alpha vee beta \$
Biconditional Elimination
\$ alpha harr beta \ \ |-- \ \ (alpha rarr beta) wedge (beta rarr alpha) \$
De Morgan’s Law
\$ not (alpha wedge beta) \ \ |-- \ \ not alpha vee not beta \$
\$ not (alpha vee beta) \ \ |-- \ \ not alpha wedge not beta \$
Distributive Property
\$ alpha wedge (beta vee gamma) \ \ |-- \ \ (alpha wedge beta) vee (alpha wedge gamma) \$
\$ alpha vee (beta wedge gamma) \ \ |-- \ \ (alpha vee beta) wedge (alpha vee gamma) \$
Resolution
\$ alpha vee beta \ , not alpha \ \ |-- \ \ beta \$
\$ alpha vee beta_1 vee beta_2 vee ... vee beta_n \ , not alpha \ \ |-- \ \ beta_1 vee beta_2 vee ... vee beta_n \$
\$ alpha vee beta \ , not alpha vee gamma \ \ |-- \ \ beta vee gamma \$
\$ alpha vee beta_1 vee beta_2 vee ... vee beta_n \ , not alpha vee gamma_1 vee gamma_2 vee ... vee gamma_m \ \ |-- \ \ beta_1 vee beta_2 vee ... vee beta_n vee gamma_1 vee gamma_2 vee ... vee gamma_m \$
Theorem Proving
Conversion to CNF
A KB can be converted into CNF with he following Algorithm:
- Eliminate biconditionals:
turn \$ ( alpha harr beta ) \$ into \$ ( alpha rarr beta ) wedge ( alpha rarr beta )\$ - Eliminate implications:
turn \$ ( alpha rarr beta ) \$ into \$ ( not alpha vee beta ) \$ - Move \$ not \$ inwards using De Morgan’s Laws:
turn \$ not ( alpha wedge beta ) \$ into \$ ( not alpha vee not beta ) \$ - Use distributive law to distribute ∨ wherever possible
Inference by Resolution
To determine if \$BK |-- alpha\$ we check \$ (KB wedge not alpha) \$
- convert \$ KB wedge not alpha \$ into Conjunctive Normal Form
- use resolution to create new clauses
- if ever we produce the empty clause (equivalent to
false
), we have a contradiction, and \$ KB |-- alpha \$ - if we can’t produce any more clauses there is no entailment
- if ever we produce the empty clause (equivalent to
First order logic
Is a more expressive logical framework than propositional logic and adds new components:
- Predicates that describe properties
- Quantifier
- Universal Quatifier \$forall\$
- Exists Quatifier \$exists\$