Inference in First-Order Logic - Department of Computer ...

[Pages:51]Inference in First-Order Logic

Philipp Koehn 12 March 2019

Philipp Koehn

Artificial Intelligence: Inference in First-Order Logic

12 March 2019

A Brief History of Reasoning

1

450B.C. 322B.C. 1565 1847 1879 1922 1930 1930 1931 1960 1965

Stoics Aristotle Cardano Boole Frege Wittgenstein Go? del Herbrand Go? del Davis/Putnam Robinson

propositional logic, inference (maybe) "syllogisms" (inference rules), quantifiers probability theory (propositional logic + uncertainty) propositional logic (again) first-order logic proof by truth tables complete algorithm for FOL complete algorithm for FOL (reduce to propositional) ? complete algorithm for arithmetic "practical" algorithm for propositional logic "practical" algorithm for FOL--resolution

Philipp Koehn

Artificial Intelligence: Inference in First-Order Logic

12 March 2019

The Story So Far

Propositional logic

Subset of propositional logic: horn clauses

Inference algorithms ? forward chaining ? backward chaining ? resolution (for full propositional logic)

First order logic (FOL) ? variables ? functions ? quantifiers ? etc.

Today: inference for first order logic

Philipp Koehn

Artificial Intelligence: Inference in First-Order Logic

2 12 March 2019

Outline

Reducing first-order inference to propositional inference Unification Generalized Modus Ponens Forward and backward chaining Logic programming Resolution

Philipp Koehn

Artificial Intelligence: Inference in First-Order Logic

3 12 March 2019

4

reduction to propositional inference

Philipp Koehn

Artificial Intelligence: Inference in First-Order Logic

12 March 2019

Universal Instantiation

5

Every instantiation of a universally quantified sentence is entailed by it: v

SUBST({v g}, )

for any variable v and ground term g

E.g., x King(x) Greedy(x) Evil(x) yields

King(John) Greedy(John) Evil(John) King(Richard) Greedy(Richard) Evil(Richard) King(F ather(John)) Greedy(F ather(John)) Evil(F ather(John))

Philipp Koehn

Artificial Intelligence: Inference in First-Order Logic

12 March 2019

Existential Instantiation

6

For any sentence , variable v, and constant symbol k that does not appear elsewhere in the knowledge base: v SUBST({v k}, )

E.g., x Crown(x) OnHead(x, John) yields Crown(C1) OnHead(C1, John)

provided C1 is a new constant symbol, called a Skolem constant

Philipp Koehn

Artificial Intelligence: Inference in First-Order Logic

12 March 2019

Instantiation

7

Universal Instantiation ? can be applied several times to add new sentences ? the new KB is logically equivalent to the old

Existential Instantiation ? can be applied once to replace the existential sentence ? the new KB is not equivalent to the old ? but is satisfiable iff the old KB was satisfiable

Philipp Koehn

Artificial Intelligence: Inference in First-Order Logic

12 March 2019

 ................
................

In order to avoid copyright disputes, this page is only a partial summary.

Google Online Preview   Download