Chapter 3: Golden Years, Physical Symbol System Hypothesis Flashcards
Which period was said to be the golden years of AI? List 4 features that contributed to this designation
The golden years of AI were between 1955 and 1974. In that period there was:
- Lots of funding
- Many promises and optimism
- Symbolic AI the prevailing method
- Artificial General Intelligence was often the end goal.
Keywords: 1955, 1974, funding, optimism, symbolic AI, AGI.
When is a physical system a physical symbol system?
When it:
- Contains a number of symbols
- Contains expressions consisting of symbols and their relations
- Contains processes/rules that manipulate these expressions, in particular create new expressions.
Keywords: symbols, expressions, rules, creation
Define the Physical Symbol System Hypothesis. Explain the key terms of this definition.
A physical symbol system has the necessary and sufficient means for general intelligent action.
- Necessary means that all general intelligent beings are physical symbol systems
- Sufficient means that all physical symbol systems (of sufficient size) can be made in such a way to perform general intelligent actions.
E.g.
1. Humans brains are a physical symbol system
2. Modern computers can exhibit general intelligent action
Keywords: necessary, sufficient, criterion, intelligence
Give an example of a computer program that is deemed a physical symbol system.
Logic theorist, created by Newell & Simon. Made to prove mathematical theorems.
(Other examples include: logical agents, SRHDLU, ELIZA)
How is information encoded in logical agents?
Information is encoded into a knowledge base (KB) using first-order logic formulas. Logically, KB is a conjunction of formulas:
KB=φ1 ∧ φ2 ∧ · · · ∧ φn
Where y φi is a logical formula asserting some “knowledge”.
Keywords: knowledge, first-order logic, conjunction
Provide the logical equivalence of the following formulas:
- φ → ψ
- ¬(φ ∧ ψ)
- ∀X : φ
- ∃X : φ
- ¬φ ∨ ψ
- ¬φ ∨ ¬ψ
- ¬∃X : ¬φ
- ¬∀X : ¬φ
What would be a naive way to prove a logical theorem? Provide two requirements for this approach, and explain the caveat.
We could systematically apply first-order logical rules to the KB until we find ϕ or ¬ϕ. This approach essentially just enumerates all theorems that follow from the KB, and that it will only work if the inferences rules are complete (i.e. they can deduce all logically valid statements) and sound (i.e. they do not generate any false statements).
This is the best we can do, since first-order logic is only semi-decidable, meaning that there is no algorithm that can determine the truth or falsehood of all statements in first-order logic. (Undecidability of a statement does not depend on the specific KB that is being used, but rather on the properties of first-order logic itself)
Keywords: first-order logic, enumerate, completeness, soundness, semi-decidability.
Explain refutation-based methods for proving logical theorems.
Refutation-based methods essentially use proof by contradiction:
- Add ¬ϕ to KB to get KB ∧ ¬ϕ
- Attempt to show that KB ∧ ¬ϕ is invalid
Explain how truth values are assigned to (syntactical) formulas. Also explain satisfiability and validity.
A logical formula φ only has a truth value with respect to a given model M. A model provides an interpretation of the logical formula, and the truth value of the formula is assigned based on the evaluation of the formula under that interpretation.
- “Satisfiability” refers to the ability of a formula to be true for at least one model (existential).
- “Validity” refers to the ability of a formula to be true for all models (universal).
If a logical formula is unsatisfiable, it is also invalid.
Keywords: models, interpretation, truth, existential, universal
What is the difference between an atom and a literal? Furthermore, define clauses and ‘clausal form’.
- An atom is a predicate, whereas a literal is an atom, or an negation of an atom.
- A clause is a disjunction of literals:
( C = L1 ∨ · · · ∨ Ln) - A formula is in clausal form if it is in a conjunction of clauses:
(C1 ∧ · · · ∧ Cn)
Practice: are these formulas in clausal form?
- (A ∨ B ∧ C) ∧ (¬A ∨ C)
- (A(X) ∨ B(Y )) ∧ (¬A(Y ) ∨ B(X))
- ∃X : ¬P(X) ∨ Q(X)
- No, left conjunct is not a clause
- Yes, both conjuncts are clauses
- No, formula contains an existential quantifier
Explain the goal and process of Skolemization.
Skolemization is a technique used in predicate logic to eliminate the existential quantifiers in a formula by introducing new function symbols, known as Skolem functions. The process of Skolemization is used to convert a formula in the prenex normal form, which is a formula that has all quantifiers at the front, into clausal form, which is a disjunctive normal form of a formula that is composed of clauses.
The process of Skolemization replaces every existentially quantified variable X with a function f (·) whose arguments are the universally quantified variables that have X in their scope, for example:
∃x (P(x) ∧ Q(x)) becomes P(f(x)) ∧ Q(f(x))
(or P(c) ∧ Q(c), if written as a Skolem constant, applicable when the skolem function has no arguments)
Two things to keep in mind;
- The names of the Skolem functions must be unique
- This process preserves satisfiability but not validity
Practice: Skolemize the below formulas:
1. ∃X : ∀Y : P(X, Y )
2. ∀X : ∀Y : ∃Z : P(X, Y , Z)
3. ∃X : ∀Y : ∃Z : P(X, Y , Z)
- ∀Y : P(c, Y )
- ∀X : ∀Y : P(X, Y , f(X, Y))
- ∀Y : P(c, Y , f(Y))
Provide the 6 rules for rewriting a formula into clausal form.
- Move all negations inward until only atoms are negated
- Rename all variables so that they are unique per quantifier
- Get rid of existential quantifiers by Skolemization
- Make all quantifiers implicit
- Convert to conjunctive normal form by distributing disjunctions and conjunctions
- Write down the clauses in a list
Keywords: negations, rename, uniqueness, Skolemization, implicit, conjunctive normal form, list
Describe the resolution inference rule.
The resolution inference rules takes two clauses and produces a new clause. The input clauses must contain a complementary literal. An example:
L1 ∨ · · · ∨ Ln ∨ S and M1 ∨ · · · ∨ Mm ∨ ¬S resolves to:
L1 ∨ · · · ∨ Ln ∨ M1 ∨ · · · ∨ Mm, which is called the resolvent of the inputs.