Vincec's Dimension

AI Review Note - Logic

Word count: 1,878 / Reading time: 12 min
2018/10/23 Share

Logic

Logic are formal languages for represting information such taht conclusions can be drawn

Syntax defines the sentences in the language

Semantics define the “meaning” of sentences

Type of Logic

  • Propositional logic [Facts]
  • First-Order Logic (FOL) [Facts, objects, relations]
  • Temporal Logic [Facts, objects, relations, times]
  • Probability theory [Facts, in degree of belief (0, 1)]
  • Fuzzy Logic [Facts, in degree of truth (0, 1)]

Inference (⊢ / provable)

KB ⊢ a, _a_ can be derived from _KB_ by procedure.

  • People make inference from what we know so far
  • Inference is a the process of finding the entailment
  • Inference is determining if entailment is true or not
  • False ⊢ True is True

CMU source: [6]

  • An inference algorithm is a procedure for deriving a sentence from the KB
  • KB ⊢ i S means that S is inferred from KB using algorithm i.
  • The inference algorithm is sound if it derives only sentences that are entailed by KB.
  • The inference algorithm is complete if it can derive any sentence that is entailed by KB.

Soundness

  • Procedure i is sound: whenever KB ⊢ a, it is also true KB ⊨ a (It guarantees that KB indeed entails a)
  • Produce only entailed sentences
  • Not infer the false sentences

Completeness

  • Procedure i is complete: Whenever KB ⊨ a, it is also true that KB ⊢ a (Finding any sentence a that is entailed by KB)
  • Produce all entailed sentences
  • Derives any sentences that is entailed

Entailment (⊨)

KB ⊨ a: _KB_ entail sentence _a_, iff, _a_ is true in all worlds where _KB_ is true. (KB contains “A Won”, “B Won”, entails “Either A or B won”)

  • It is impossibal premises(前提) are true and consequence if false.
  • KB inference a → sound → KB entails a → complete → KB inference a → …
  • False ⊨ True is True

CMU source: [6]

  • “KB logically entails S” if all the models that evaluate KB to True also evaluate S
    to True.
  • Denoted by: KB ⊨ S
  • Note: We do not care about those models that evaluate KB to False. The result of evaluating S for these models is irrelevant.

Model

If a sentence _a_ is true in model _m_, we say m satisfies a, or m is a model of a (the real world model satisfies the statment in our head)

  • M(a) is the set of all models of _a_
  • M(KB) is the set of all models of KB(KnowledgeBase)
  • KB ⊨ a iff(if and only if) M(KB) is a subset M(a)

Propositional Logic

Symbols (wiki)

Boolean Variables:

  • True (⊤ or 1)
  • False (⊥ or 0)

Sentences (either true or false)

  • Atomic sentences / single proposition symbol
  • Complex sentences / one or more propositions with logical connectives

Literal

An atomic sentence or its negation

  • Positive literal: p
  • Negative literal: ¬p / ˜p / !p

Not (¬ / ~ / !)

Negation

And (∧ / · / &)

Conjunction: A sentence whose main connective is And.

  • (P∧Q)∧(R∧S)∧(T∧U) is conjunction.

Or (∨ / + / ||)

Disjunction: A sentence whose main connective is Or.

  • (P∧Q)∨(R∧S)∨(T∧U) is disjunction.

Implies (⇒ / → / ⊃)

Means Implication:

  • Antecedent (前情) → Consequent
  • Only False when: True → False

Biconditional (⇔ / ≡ / ↔), iff

Means Equivalence

  • True when boths side are true or both sides are false

Syntax

Illustrates the basic ideas / sentences relationships

Semantics

The meanings / value of the each propostion based on the current model

Truth Table


Entailment proof

  • set of true sentences, KB
  • join as a big conjunction
  • create a truth table
    verify sentence

Algorithm is sound: it directly implements the definition of entailment.
Algorithm is complete: it works for any sentence and always terminates

Enumeration Method

Check all possible models - a must be true wherever KB is true

Validity

If the sentence is true in all models

a is valid iff ~a is unsatisfiable

Satisfiable

If the sentence is true in at least one models

a is satisfiable iff ~a is not valid

Entailment as satisfiability

  • a ⊨ b iff the sentence (a ⇒ b) is valid
  • (a ⇒ b) is valid iff ¬(a ⇒ b) is unsatisfiable
  • ¬(a ⇒ b) ⇔ ¬(¬a ∨ b) ⇔ (a ∧ ¬b)
  • a ⊨ b iff (a ∧ ¬b) is unsatisfiable

Tautology

A sentence that is necessarily True, in all models. ((P⇒Q)⇔(¬P∨Q))

De Morgan Laws

  • (P ∧ Q) ∨ (R ∧ S)
  • ¬(¬(P ∧ Q)) ∨ ¬(¬(R ∧ S))
  • ¬(¬P ∨ ¬Q)) ∨ ¬(¬R ∨ ¬S))

Inference Rules

Requires sentences to be in horn form

  • Modus Ponens
    • (a ⇒ b, a) ⇒ b
  • Modus Tollens
    • (a ⇒ b, ¬b) ⇒ ¬a
  • And-Elimination
    • (a1 ∧ a2 ∧ a3 ∧ a4… an) ⇒ (ai)
  • And-Introduction
    • (a1, a2, a3, a4… an) ⇒ (a1 ∧ a2 ∧ a3 ∧ a4… an)
  • Or-Introduction
    • (ai) ⇒ (a1 ∨ a2 ∨ a3 ∨ a4… anb)
  • Double-Negation Elimiation
    • ¬(¬a) ⇒ a
  • Contraposition
    • (a ⇒ b) ⇒ (¬b ⇒ ¬a), - (¬a ⇒ ¬b) ⇒ (b ⇒ a)
  • Unit Resolution
    • (a ∨ b, ¬b) ⇒ (a)
    • (a1 ∨ a2 ∨ a3…an, m, which _ai_ and _m_ is complementary literals) ⇒ (a1 ∨ a2 ∨ a3 ∨ a4… a(i-1) ∨ a(i+1) … ∨ an)
  • Resolution
    • (a ∨ b, ¬b ∨ c) ⇒ (a ∨ c)
    • (¬a ⇒ b, b ⇒ c) ⇒ (¬a ⇒ c)
    • (a1 ∨ a2 ∨ a3…ak, m1 ∨ m2 ∨ m3…mn, which _ai_ and _mj_ is complementary literals) ⇒ (a1 ∨ a2 ∨ a3 ∨ a4… a(i-1) ∨ a(i+1) … ∨ ak ∨ m1 … m(j-1) ∨ m(j+1) … ∨ mn)

Found CNF Three Examples:

  • (a ∧ b) V (b ∧ c) ⇒ (a ∨ b) ∧ (a ∨ c) ∧ b ∧ (b ∨ c)
  • (a ∨ b) ∧ (b ∨ c)
  • (a ∨ b) ∧ (¬b ∨ c) ⇒ (a ∨ c)

Horn Clause

a Horn clause is a clause (a disjunction of literals ) with at most one positive literal(<=1)…a Horn clause with no positive literals is sometimes called a goal clause [1]

  • E.g. ¬P ∨ ¬Q ∨ ¬R ∨ ¬S, or P ∧ Q ∧ R ⇒ ¬S(implication form)
  • KB ∧ ¬a, is still a horn clause

Definite Clause [4]

A Horn clause with exactly one positive literal is a definite clause.

Fact

a definite clause with no negative literals is sometimes called a fact

Goal clause

a Horn clause without a positive literal is sometimes called a goal clause

Forward Chaining

Start with horn clause

Downside: effiency / Good for maintain

Backward Chaining

Start with conclusion

More target

First-Order Logic

Aviod ambiguous, keep, declarative and compositional of propositional logic

FOL is built around objects and relations. FOL can express facts about some or all objects in the universe.

Propostional VS FOL:

  • P: YES/NO; May multiple queries (e.g. Is it 5PM?)
  • FOL: Answer is not limited with YES/NO; Only single query (e.g. What time is it?)
  • They are both monotonic

Syntax

Symbols

  • Constant - objects
  • Predicate - relations or property, return True ro false
    • e.g. Bites(Man, Dog): Predicate(arguments)
  • Function - relates objects to one other objects, return values
  • Conventions - Upper-case letters

Arity

The number of arguments for given predicate

  • Binary predicates, e.g. HigherThan(A, B)
  • Unary predicates, e.g. High(A)
  • Nullarity predicates, e.g. MadeOfCheese()

Terms

A logic expression that refer to an object

Variables

Terms or argument of a function, in lowercase

Functions

Refer to domain objects, like Constants and Variables, look similar to predicates but returns value/objects instead of True/False

  • Constants refer directly to domain objects
    • E.g. Richard, John, Dog
  • Variables refer to the conjunction or disjunction of domain objects
    • E.g. ∀x, ∃y, A ∧ B ∧ C
  • Functions refer indirectly to domain objects using other terms
    • E.g. LeftLeg(Richard), G(x, y)

Sentence

Atomic Sentence

interpreted with repect to a model / contain no variables or conjunctions [5]

  • E.g. Bites(A, B)

Complex sentences

One or more predicate-argument relations.

  • E.g. Bites(A, B) ∧ Owns(A, B)

Quantifiers

  • Univeral quantification(∀)
  • Existential quantification(∃)

∃ x (owns(A, B) ∧ Bites(A, B))
Quantifiers + variable + variable scope

Nested Quantifiers

  • ∀x ∀y ⇔ ∀x ∀y
  • ∃x ∃y ⇔ ∃x ∃y
  • ∀x ∃y P(x, y) ⇔ ∀x (∃y P(x, y))

Quantifier Negation

∀x P ⇔ ¬∃y ¬P

Propositionalization

  • Convert FOL KB into propositional KB
  • Every FOL KB can be propositionalized

Problems

  • Exponential Space
  • Generating irrelevant sentences
  • Infinite Terms in Function
  • Lterative Deepening
  • Herbrand’s Theoren: if no proof will infinite loop.

Unify Operator

  • Given(two sentences)
  • Return(A unifier of the two sentences with substitution OR Fail if no substitution exists)

    Most Genernal Unifier(MGU)

    A sound inference rule.

Forward Chaining

  • Start from known facts
  • Sound and Complete
  • Datalog

Backward Chaining

  • Aviod loops
  • Aviod repeated work
  • Linear Size of Proof Space
  • Soundness by using Generalized Modus Ponens (GMP)
  • Incomplete due to infinite loops
  • Prolog(Prolog is not soundness, lacking occur check)

Prolog Example:

A useful programming/prototyping paradigm; A Prolog program is a set of Horn clauses

Aviod infinite loops in Prolog

  1. path(X, Z) :- link(X, Z) / Check the stop condition first
  2. path(X, Z) :- path(X, Y), link(Y, Z)

Conjunctive Normal Form (CNF)

A conjunction of clauses, each clasue being a disjunction of literals. It is always possible to convert any KB to CNF

Steps:

  1. Eliminate ⇒ (A ⇒ B -> ¬ A ∨ B)
  2. Move ¬ inward
  3. Standardize variables e.g. import z if have two y
  4. Skolemization replace ∃ with Function Q()
  5. Drop Universal Quantifiers remove ∀
  6. Distribute ∨ over ∧

Special-Purpose Logics

  • Temporal logic
  • Higher-order logic(HOL)

Knowledge Engineering

Declarative (陈述)

Ontology

Concepts/Categories

Defining Concepts/Categories

  • A is a necessary condition for B iff B⟹A. In other words, it cannot be true that B holds while A doesn’t 2.
  • P is a sufficient condition for Q iff P⟹Q. In other words, as soon as P holds, we know that Q holds as well 2.
  • Necessary and Sufficient Conditions

Representing Concepts/Categories

  • Represent as unary predicate
    • E.g.
    • Categories: Ace(x), Basketball(x)
    • Membership: Basketabll(x1)
    • Subclass: ∀x Ace(x) ⇒ Card(x)
  • Represent as an object itself. (E.g. )
    • E.g.
    • Categories: Aces, Basketballs
    • Membership: B1 ∈ Basketablls
    • Subclass: Aces ⊂ Cards / Aces ⊆ Cards

Subclass

Type Hierarchies (?Is-a hierarchy)

Referred as an ontology, a taxonomy

Allows Inheritance type of reasoning, Inheritance can occur from any superclass

PartOf Hierarchies

Allows Transitivity type of reasoning.

Planning 3

Situation

A Situation is a logical term; Result(Action, Situation)

Fluents

A Fluent is a function or a predicate that vary from one situation to the next. By convention, the situation is always the last argument of the fluent. (Change with time/situation)

Atemporal predicates/functions

An atemporal predicate/function is a predicate/function that do not vary from one situation to the next. (not change with time/situation)

Classic Issues

  • Frame Problem
    • Represent all things
    • Closed-world is help to deal with it/ not a solution
  • Qualification problem
    • Qualification
  • Ramification Problem
    • Side effect

      Planning Language

  • State
  • Goals
  • Actions

    Representing goals

  • Conjunction of positive literals
  • Goal is satisifed if state contains all literals

    Representing actions

  • Action
    • Name + parameters + precondition + effect (E.g. (Fly(p, from, to)))
  • Precond: …
    • must be true
  • Effect: …
    • Conjunction of function-free positive literals
    • Positive literals add facts / Negative literals remove facts
    • Can represent as Add: At(p, to) / Delete: At(p, from)

Planning Domain Definition Language (PDDL)

Planning with State-Space Search / Whole Order Plan (NP hard)

  • Forward: Progression (A* or iternative deepening from start)
  • Backware: Regression (From goal)

Partial-Order Planning (POP)

  • State (Initial State or Goal State )
  • Actions (step in the plan)
  • Orderings (set of ordering constraints: A < B(A before B)>)
  • Links (Set of Casual links)
  • Open (set of Open preconditions)

Planning Graph

Consisting of a sequence of levels that correspond to steps in the plan, Works only for Propositional plainning problems with no varibles
State0 + Action0 + State1 + Action1 +…

  • Literals (increase monotonically)
  • Actions (increase monotonically)
  • Conflicts
  • Mutex Relations (decrease monotonically)

No Solution: all goals present & non-mutex or extrasolution fails

Referece:

CATALOG
  1. 1. Logic
  2. 2. Type of Logic
  3. 3. Inference (⊢ / provable)
    1. 3.1. Soundness
    2. 3.2. Completeness
  4. 4. Entailment (⊨)
  5. 5. Model
  6. 6. Propositional Logic
    1. 6.1. Symbols (wiki)
    2. 6.2. Sentences (either true or false)
    3. 6.3. Literal
    4. 6.4. Not (¬ / ~ / !)
    5. 6.5. And (∧ / · / &)
    6. 6.6. Or (∨ / + / ||)
    7. 6.7. Implies (⇒ / → / ⊃)
    8. 6.8. Biconditional (⇔ / ≡ / ↔), iff
    9. 6.9. Syntax
    10. 6.10. Semantics
    11. 6.11. Truth Table
    12. 6.12. Entailment proof
    13. 6.13. Enumeration Method
    14. 6.14. Validity
    15. 6.15. Satisfiable
    16. 6.16. Entailment as satisfiability
    17. 6.17. Tautology
      1. 6.17.1. De Morgan Laws
  7. 7. Inference Rules
    1. 7.1. Horn Clause
      1. 7.1.1. Definite Clause [4]
      2. 7.1.2. Fact
      3. 7.1.3. Goal clause
      4. 7.1.4. Forward Chaining
      5. 7.1.5. Backward Chaining
  8. 8. First-Order Logic
    1. 8.1. Syntax
      1. 8.1.1. Symbols
      2. 8.1.2. Arity
      3. 8.1.3. Terms
      4. 8.1.4. Variables
      5. 8.1.5. Functions
      6. 8.1.6. Sentence
        1. 8.1.6.1. Atomic Sentence
      7. 8.1.7. Complex sentences
      8. 8.1.8. Quantifiers
      9. 8.1.9. Nested Quantifiers
        1. 8.1.9.1. Quantifier Negation
  9. 9. Propositionalization
    1. 9.1. Problems
  10. 10. Unify Operator
    1. 10.1. Most Genernal Unifier(MGU)
  11. 11. Forward Chaining
  12. 12. Backward Chaining
    1. 12.1. Prolog Example:
      1. 12.1.1. Aviod infinite loops in Prolog
  13. 13. Conjunctive Normal Form (CNF)
  14. 14. Special-Purpose Logics
  15. 15. Knowledge Engineering
    1. 15.1. Ontology
    2. 15.2. Defining Concepts/Categories
    3. 15.3. Representing Concepts/Categories
    4. 15.4. Subclass
      1. 15.4.1. Type Hierarchies (?Is-a hierarchy)
      2. 15.4.2. PartOf Hierarchies
  16. 16. Planning 3
    1. 16.1. Situation
    2. 16.2. Fluents
    3. 16.3. Atemporal predicates/functions
    4. 16.4. Classic Issues
    5. 16.5. Planning Language
      1. 16.5.1. Representing goals
      2. 16.5.2. Representing actions
    6. 16.6. Planning Domain Definition Language (PDDL)
    7. 16.7. Planning with State-Space Search / Whole Order Plan (NP hard)
    8. 16.8. Partial-Order Planning (POP)
    9. 16.9. Planning Graph
  17. 17. Referece: