[인공지능] Chapter 5. Propositional logic

• Propositional Logic 명제 논리
  • Basic concepts of knowledge, logic, reasoning
  • Propositional logic: syntax(구문) and semantics(의미론), Pacworld example
  • Inference by model checking and theorem proving
• Agents that know things
  • Agents는 지각, 학습, 언어를 통해 지식을 습득
    • Knowledge of the effects of actions
      • trainsition model
    • Knowledge of how the world affects sensors
      • sensor model
    • Knowledge of the current state of the world
  • Can keep track of a partially observable world
  • Can formulate plans to achieve goals
• Knowledge
  • Knowledge base = set of sentences in a formal language
  • Declarative approach to building an agent (or other system)
    • Tell it what it needs to know (or have it Learn the knowledge)
    • then it can Ask itself what to do (answers should follow from the KB)
  • Agents can be viewed at the knowledge level (what they know, regardeless of how implemented)
  • 단일 추론 알고리즘으로 모든 답변 가능한 질문에 답할 수 있음

Logic

• Syntax
  • What sentences are allowed?
• Semantics
  • What are the possible worlds?
  • Which sentences are true in which worlds?
• Different kinds of logic
  • Propositional logic 명제 논리
    • 연언기호와 부정기호 만을 사용하여 추론하는 논리학
  • First-order logic
  • Relational databases

Inference: Entailment

• Entailment
  • a |= b
    • ‘a entails(involves) b’, ‘b follows from a’
    • a-worlds are a subset of the b-world

Inference: Proofs

• Proof
  • a와 b 사이의 entailment를 증명하는 것
• Sound algorithm
  • Everything it claims to prove is in fact entailed
  • 증명한다고 주장하는 모든 것이 실제로 entail됨
• Complete algorithm
  • Everything that is entailed can be proved
  • entail되는 모든 것들을 증명할 수 있음
• Method
  • Model-Checking
    • 모든 가능한 세계에서, a가 참이면 b도 참이다
    • Propositional logic 에서는 OK
    • First-order logic 에서는 not easy
  • Theorem-proving
    • a에서 b로 이어지는 증명 단계(추론 규칙의 적용)의 탐색

 

Satisfiability and Entailment

• A sentence is satisfiable
• if it is true in at least one world
• Suppose we have a hyper-efficient SAT solver;
• how can we use it to test entailment
• So, add the negated conclusion to what you know,also known as reductio ad absurdum
• test for satisfiability;
• Effiecient SAT solvers operate on conjunctive normal form

Conjunctive Normal Form (CNF)

• Every sentence can be expressed as a conjunction of clauses
• Each clause is a disjunction of literals
• Each literal is a symbol or a negated symbol
• Conversion to CNF by a sequence of standard transformations

State estimation

• 주어진 관찰과 행동 이력을 바탕으로 현재 무엇이 참인지 추적하는 것
• A logical agent can just ask itself!
• ‘Lazy’
  • it analyzes one’s whole life history at each step

Summary

• One possible agent architecture
  • knowledge + inference
• 논리는 지식을 인코딩하는 공식적인 방법
  • 논리: syntax(구문), set of possible worlds(가능한 세계 집합), truth condition(진리 조건)
• A simple KB for Pacman
  • covers the inital state, sensor model, and transition model
• 논리적 추론은 문장 간의 entailment 관계를 계산하여 광범위한 작업을 수행
• DPLL 기반의 SAT solver는 매우 효율적인 추론을 제공
• Logical agents는 하나의 knowledge base에서 하나의 generic inference algorithm을 사용하여 localization, mapping, SLAM, planning (and many other things)을 수행한다.