L3: Golden Years & Physical Symbol System Hypothesis, Reasoning by Resolution & Unification

Question 1

What is the Physical Symbol System Hypothesis?

Answer 1

A physical symbol system has the necessary and sufficient means for general intelligent action.

Corollary 1
Human brains are a physical symbol system.
Corollary 2
Modern computers can exhibit general intelligent action.

Question 2

What is a knowledge base?

Answer 2

A “knowledge base” (KB) encoding information in first-order logic formulas
* Logically, KB is just a conjunction of formulas KB=φ1 ∧ φ2 ∧ .. ∧ φn
* Every φi is a logical formula asserting some “knowledge

Question 3

Want to find out whether KB models a query formula phi, how should we not do this?

Answer 3

If you apply the first order logic rules to KB then will enumerate all theorems that follow, but phi and not phi might not be entailed by KB. Then algorithm will never terminate (have to assume KB to be infinite).

This is always the case as first-order logic is semi-decidable, might never terminate

Question 4

How would a refutation-based method work?

Answer 4

Use proof by contradiction. Do KB and not phi and attempt to show this is invalid

Question 5

What is needed to give a truth value to a formula?

Answer 5

A model which assigns truth values to formulas in KB

Question 6

What is the definition of phi being satisfiable?

Answer 6

If there is a model M such that M models phi

If unsatisfiable then also invalid

Question 7

What is the definition of phi being valid?

Answer 7

If for every model M, M models phi (e.g. p -> p)

Therefore (not phi) is unsatisfiable

Question 8

Definition of atom, literal, clause

Answer 8

• An atom is a predicate (statement)
• A literal is either an atom or the negation of an atom;
• A clause is a disjunction of literals (using OR only)

Question 9

When is a formula in clausal form?

Answer 9

Conjuction of clauses (conjuctive normal form), written as a list of clauses

Question 10

What is the relationship between a formula phi and its counterpart psi in clausal form?

Answer 10

For any formula phi there is a formula psi in clausal form s.t. phi and psi are equisatisfiable. But validity of phi does not mean validity of psi (if model for one then there will be model for second but if all models for first does not mean all models for second)

Skolemization preserves satisfiability but not validity

Question 11

How to get rid of existential quantifiers?

Answer 11

Skolemization

Replace every existentially quantified variable X with a function f (·) whose arguments are the universally quantified variables that have X in their scope.
* These replacement functions are called Skolem functions.
* A Skolem function without arguments is called a Skolem constant.
* The names of these Skolem functions must be new and unique.

Question 12

What are the rules for rewriting in the clausal form?

Answer 12

1. Move all negations inward until only atoms are negated.
2. Rename all variables so that they are unique per quantifier (i.e. if need to resolve A(X) and A(f(X)) can make second A(f(Y)) and then do the substitution f(Y)/X on both to make them equal).
3. Get rid of existential quantifiers by Skolemization.
4. Make all quantifiers implicit.
   * Due to previous step, only universal quantifiers remain.
5. Convert to conjunctive normal form by distributing disjunctions and conjunctions.
6. Write down the clauses in a list.

Question 13

What is resolution?

Answer 13

The resolution inference rule takes two clauses and produces a new clause.

The input clauses must contain a complementary literal.

Remove contradictory OR elements (because P or not P just resolves to True) and then OR everything else

Resolution derivation, applying resolution to two clauses in list C and then appending resolvent to C (or discarding if already have it) and then repeat

Question 14

What happens if resolve singleton clauses S and not S

Answer 14

Get empty clause, this is (by definition) unsatisfiable. A list of clauses is unsatisfiable if by resolution it produces the empty clause

Question 15

What are the terms in a formula?

Answer 15

A constant, variable or function (not and/ or etc.)

Question 16

What are the rules for substitution composition?

Answer 16

Apply theta 2 to theta 1 (only upper elements)
Concatenate new theta 1 and theta 2
Remove elements from new theta 1 where upper = lower and remove from theta 2 where lower in theta 1

Question 17

What is a unifier?

Answer 17

A substitution that makes two atoms equal syntactically (usually do it so we can resolve). Still have to apply substitution to other terms in clause!

MGU is usually I think the most obvious unifier

Question 18

Describe how we prove the validity of a formula with resolution

Answer 18

To prove that a formula φ is valid:
1. Take the negation ¬φ
2. Put ¬φ in clausal form and collect clauses in C
3. Find a resolution derivation of {} using unification where needed
* This step may, in general, never terminate.
4. This implies that ¬φ is unsatisfiable, whence φ is valid.

Question 19

Definition of Horn clause, definite and goal clause

Answer 19

Horn clause- at most one positive literal
Definite clause - one positive literal (non singleton definite = rules- ->, singleton definite = facts)
Goal clause- no positive literal

Assume KB is a conjuction of Horn clauses, and assume negated query can be written as such too (NOT ALWAYS TRUE, trading in expressive power to enable SLD!)

Question 20

What is Selective Linear Definite Clause Resolution?

Answer 20

The SLD-resolution rule is just resolution applied to a definite clause and a goal clause.

Always results in goal clause

Allows us to do tree search instead- traverse a tree of goal clauses, can use depth first search (Prolog), looking for empty set, could potentially still not terminate!

Leaf nodes either {} or have some clause with no matching input definite clauses