First Order Logic Flashcards
What are properties of Expressive Logic?
It is declarative: Separation between knowledge and control
It is expressive: Ability to handle unknown information or partially-known information
It is compositional: The meaning of a sentence is a function of the meaning of its parts
What are the shortcomings of propositional logic?
Verbosity: Stating simple facts often requires listing a large number of propositions.
Low expressiveness: Many facts cannot be expressed by propositional logic in a meaningful way.
What is a first-order interpretation?
A tuple:
(D, R1, R2, …, Rk, f1, …, fl)
- D is a set of elements and is called the domain.
- Each Ri is a relation or predicate defined on D
- Each f is a function defined on D
What is a bounded variable?
A variable occuring in a formula if it is within scope of some sub-formula. If a variable is not bounded, then it is called a free variable
What is Satisfaction Relation?
Lets have w be a sentence and I be an interpretation. We inductively define the satisfaction relation in such a way that satisfies w, written I |= q, if w is true according to the interpretation I.
What is a first-order knowledge base?
A set of first-order sentences in some signature. To define a model of FO-KB, we make the following two assumptions:
1. Closed-world assumption: if any atomic sentence is not to be known or shown to be true, then it is false.
2. Domain-closure assumption: In a model of the KB, all elements fo the domain appear as ground terms that can be expressed using constants.
What is an axiom?
The basic factual information from which useful conclusions can be derived.
What is a theorem?
Theorems are factual information derived from the axioms.
What is the inference problem?
It takes as input a KB and a formula w, and outputs whether KB |= w.
What is grounding?
- Instantiate variable with constants
- This turns a sentence into a proposition
- Then use methods for propositional logic to carry out inference.
What is lifting?
- Inference is directly applied to first-order logic formulas
- Generalise propositional methods to first-order logic
- Unification is an important task here.
What is the aim of grounding?
To reduce first-order logic inference task to propositional logic inference task.
What is the method of grounding?
Turn first-order logic sentences into equivalent propositions.
What is the terminology of grounding?
A substitution is of the form x/t where x is a variable and t is a term.
For a set S of substitutions and formula x, we use subset to denote the formula obtained by applying substitutions in S and w.
What are the observations of grounding?
A sentence without any quantifier is essentially a proposition.
We need existential sentences of the form Ex: w(x) and universal sentences of the form Vx:w(x)
What is existential instantiation?
From Ex: w(x), derive w(c), where c is a new constant symbol, called the Skolem constant and c is not the original signature.
What is universal instantiation?
From Vx: w(x) derive w(t) where t is any ground term.
Applying universal instantiation produces a sentence that is only an instance of the universal sentence.
What is Herbrand’s theorem?
If a sentence w is entailed by a first-order KB, then is is entailed by a finite subset of KB.
We may thus perform inference by propositionalisation:
1. Apply grounding rules to introduce propositions to KB.
2. Apply proposition logic inference
3. If a proof to w is not found, repeat to generate more propositions.
What is the undecidability theorem?
First-order inference is undecidable.
- If the search finds a proof, then the sentence w is indeed true
- But no algorithm exists that decides whether w is true or not.
What are the shortcomings of propositionalization?
It generates too many sentences, resulting in a very large propositional knowledge base for inference.
We need to only generate relevant sentences. This will allow us to do inference on first-order sentences.
How does a unification algorithm work?
It takes two sentences w1 and w2 and returns a substitution S, such that:
Subset(S, w1) = Subset(S, w2)
