DTAI

On this page, you can find a basic introduction to FO(ID). The tone here will be a bit informal and we will just try to get the basic ideas across. If you would be more interested in a proper scientific introduction to FO(ID) (with all the appropriate references to relevant literature and so on) we suggest you take a look at our papers section.

The contents of this section consists of answers to the following questions:

• What is FO(ID)? (short answer)
• What are inductive definitions?
• Why study inductive definitions?
• How do you write an inductive definition in FO(ID)?
• What is FO(ID)? (long answer)
• Can FO(ID) be used in practice?

These answers are supposed to form a more-or-less coherent whole when read subsequently, so feel free to just start reading right here:

What is FO(ID)? (short answer)

FO(ID) extends classical logic with inductive definitions. The result is an expressive knowledge representation language, which is easy to understand, suitable for practical applications, and integrates key concepts from nonmonotonic reasoning into a classical setting.

Why use FO(ID)?

Inductive definitions are an important kind of knowledge. FO(ID) allows all such definitions to be naturally and uniformly represented, in a way which integrates seamlessly with classical logic. As such, FO(ID) solves a well-known limitation of classical logic as a knowledge represenation tool. Moreover, by considering only a computationally feasible sublogic of first order logic and extending this with inductive definitions, we get a logic which is both expressive and still practically applicable.

The origins of FO(ID) lie in the field of (abductive) Logic Programming. However, it itegrates ideas from this domain into the classical, monotone setting of first order logic. As such, this logic provides a bridge across the conceptuel gap which seperates these two settings and can offer a clear view on what the domain of Logic Programming has to contribute to more traditional settings, such as SAT-solving.

What are inductive definitions?

We use this term in precisely the same way as a mathematician uses it. Therefore, you probably already know what it means. But just in case: a definition is simply something which tells you precisely which tuples belong to a certain relations, such as:

Inductive definitions are those definitions which define a relation in terms of itself, i.e., whether a certain tuple belongs to this relations depends on whether some other tuple belongs to it. The above definition of a triangle is not inductive, but for instance this definition of the natural numbers is:

This definition is inductive, because of the second rule, which state that whether x +1 is a natural number depends on whether x is already a natural number.

Why study inductive definitions?

Inductive definitions are a very natural thing. You encouter them all the time in mathematics. The following concepts are all typically defined by inductive definitions, just to name a few: the natural numbers, the transitive closure of a relation, the syntax of first-order logic, the truth value of a propositional formula, the fibonacci sequence, and so on. However, inductive definitions do not only occur in mathematics. Indeed, in common-sense reasoning, one can find just as many example of concepts which can be inductively defined. For instance, the frame axiom states that a property holds if it already held previously and was not terminated. A state is reachable if it is the result of executing an action in a state which was already reachable.

All in all, it is quite clear that inductive definitions are a distinctive and important kind of knowledge. As such, if you want to write down your knowledge about a certain domain in a formal logic, chances are good that you will end up needing to express some inductive definitions. Doing this in classical logic is quite hard. In first-order logic, for instance, it is already impossible to define a simple transitive closure. One could of course move to second-order logic, but even there it is not possible to come up with a general way of uniformly representating inductive definitions. In a sense, the ability to express inductive definitions is simply missing from classical logic. This observation has been made before (see below) and has given rise to a number of different extensions of classical logic. Of these, FO(ID) offers the most general formalization, in the sense that all kinds of definitions which appear in mathematics can be naturally represented.

How do you write an inductive definition in FO(ID)?

This is really quite easy. Basically, if you are able to write an inductive definition "in words", i.e., in such a way as one would do this in a mathematical text, you can also write it in FO(ID). To see how this is done, let's start by looking at an example. This is the usual definition of the transitive closure of a relation, as you would find it in a typical mathematical textbook:

Let's take a closer look at the structure of this definition.

We can distinguish the following parts:

• The definition needs some "inputs", in this case a base relation R.
• The definition then defines some concept, in this case the transitive closure of R.
• There is usually a little phrase which simply means "the following should be interpreted as an inductive definition".
• The actual definition now consists of a number of rules, typically using an "if-then" connective.

Now, let's take a look at the same definition in FO(ID).

Now, if you take a moment and compare this formula in FO(ID) to the definition above, you should see some strong similarities. FO(ID) has two connectives which are not in classical logic:

• Curly braces {} are used to indicate that an inductive definition is being expressed (cfr. the phrase "is inductively defined as" in the definition above).
• The definitional implication symbol ← can be read as "if some condition is satisfied, then by definition some tuple belongs to the relation being defined"; it plays the same role as the words "if then" in the original wording of the definition.

An inductive definition is now a set {r1, r2,... } of rules, where each rule is of the form:

with:

• x a tuple of variables;
• P(t) an atom, i.e., P a predicate and t a tuple of terms;
• φ some first order formula.

Each such rule is read as: "for all x, if φ, then by definition P(t) holds." The atom P(t) is called the head of the rule and the formula φ the body of the rule. A predicate that appears in the head of at least one rule of a definition, is said to be defined by this definition. All other predicates are called open. In the example above, the only defined predicate is the transitive closure; the predicate R is an open predicate, i.e., one which is assumed to be given.

Here is another definition in FO(ID):

This definition defines a predicate Winning_position, given the open predicate Move. In words, we would therefore read this definition as follows:

And here is yet another one:

This definition defines two relations, even and odd. In a mathematical text, attention would typically be drawn to the fact that two concepts are being defined in a single definition, by use of the term simultaneous induction, such as:

In general, every inductive definition you would encounter in mathematics, can be written down in FO(ID) in a straightforward and natural way, using the same mathodology as we have already used for all the examples in this section.

What is FO(ID)? (long answer)

As said above, FO(ID) extends classical logic with inductive definitions. Now, the term classical logic does not actually denote a single logic, but rather a family of logics of different expressivity:

• Propositional logic (also called propositional calculus)
• First-order logic
• Second-order logic
• ...

To each of these, one can add the "inductive definition"-primitive, to obtain an FO(ID) version of this particular logic. For instance, the extension of first-order logic with inductive definitions, denoted FO(ID), can be defined like this (the only difference between this definition and the definition of first-order logic one would find in a typical textbook, is the second bullet):

For instance, the following is an FO(ID)-formula:

This FO(ID)-formula is the conjunctions of two definitions (that of Grandfather and that of Son) and two first-order formulas. It is interesting to note that one is also allowed to include multiple definitions for the same concept, such as:

One can similarly define an extension of second order logic with inductive definitions, which is called SO(ID), and an extension of propositional calculus with inductive definitions, which is denoted PC(ID). In the propositional version, the formulas appearing in definitions are of course also restricted to propositional formulas.

Can FO(ID) be used in practice?

Inductive definitions are useful for practical purposes. Indeed, such definitions are essentially a constructive kind of knowledge, specifying how an interpretation of the open preedicates can be extended to the defined predicates. FO(ID) is therefore also useful from a computational point of view. The basic idea is to take some restricted subset of first-order logic with desirable computational properties and then add inductive definitions to this subset, making the logic more expressive without making inference infeasible. One such useful sublogic of FO(ID) is the Inductive Definition Programming or IDP fragement.

Here are two different inference tasks for IDP:

• Model generation: this is the most standard inference task: to find a "possible world" (or all of them) according to the given IDP theory. Here is a system that does model generation for IDP.
• Query answering: FO(ID) originates in abductive logic: the A-system is a query answering system for this.