First-Order Logic

Material from Representation and Inference for Natural Language, Patrick Blackburn and Johan Bos, 2005. Book site.

We study one method to:

Associate semantic representations with natural language expressions
Describe additional background knowledge, context and assumptions used while interpreting natural language utterances
Use the semantic representations to compute inferences and unveil implicit content conveyed by natural language utterances in context.

Vocabulary
First-order models
First-order languages
Satisfaction

Vocabulary

A first-order formula is a description of facts. A first-order model is an idealization of situations in the world. Evaluating a formula in a model verifies whether the description is true or false in the situation.

Both the model and the formula must "talk about" the same topic - individuals and relations that can hold among the individuals. The vocabulary captures this notion of aboutness:

{ (Love,2), (Customer,1), (Robber,1), (Mia, 0), (Vincent,0), (Yolanda,0) }

The numbers afer the symbols indicate the arity of the symbol - that is, how many parameters we expect to see after the symbol.

First-order models

The model is a situation corresponding to a certain vocabulary. The model contains 2 components:

The domain D: a set of individuals - the entities about which we are talking.
Semantic value: the value associated to each term in the vocabulary in the domain. This is represented by a function F, mapping words in the vocabularies to objects built from the domain.

For example, for the vocabulary above, consider the following model:

D = {d1, d2, d3, d4}
F(Mia) = d1
F(Vincent) = d2
F(Yolanda) = d3
F(Robber) = {d1, d2}
F(Customer) = {d3, d4}
F(Love) = { (d1, d2), (d3, d4) }

Note: the value of a symbol of arity 0 is an individual, of a symbol of arity one, a set of individuals, of a symbol of arity n, a set of n-tuples of individuals.

Note that not all individuals must have names (d4 has no name in the model), and an individual can have several names.

First-order languages

We define a first-order language in an inductive manner (syntactically) from the following components:

All the symbols in the vocabulary
A countably infinite collection of variables xi
Boolean connectives (negation, conjunction, disjunction, implication)
Quantifiers (forall, exists)
Parentheses

We then define inductively:

A term is any variable or constant from the vocabulary.
If R is a relation symbol of arity n, and ti are n terms, then R(t1,..,tn) is an atomic formula.
Well-formed formulas are constructed from the rules: atomic formula, not(f), f1 and f2, f1 or f2, f1 imp f2, forall(x,f), exists(x,f), (f) -- where f, f1 and f2 are well-formed formulas

We distinguish free and bound occurrences of variables in formula. A sentence is a well-formed formula that contains no occurrence of free variable.

Satisfaction

3 inference tasks can be distinguished:

The querying task: given a model, verify whether a formula is true. This is a computationally easy task. A simple variation of this task involved formula with free variables. In this case, the objective is to return variable assignments for which the formula holds wrt to the model.
The consistency checking task: this is a more abstract task. Given a set of formula {Fi}, determine whether there exists a model wrt which the conjunction of formula hold.
The informativity checking task

More information to be read in Chapter 7 "Logical Agents" of the book "Artificial Intelligence - a Modern Approach" (AIMA) by Russel and Norvig.

Code for first-order logic manipulation in Common Lisp is to be found in the Logic module of the source code of the AIMA book.

Code in Java for the same interfaces is to be found in Java code overview, Javadoc and Logic package.

Last modified June 4th, 2007