The FO[·] Language

Overview

The FO[·] (aka FO-dot) language is used to create knowledge bases. It is described in the FO-dot standard. This document presents the implementation in IDP-Z3.

An FO-dot knowledge base is a text file containing the following blocks of code:

vocabulary

specify the types, predicates, functions and constants used to describe the problem domain.

theory

specify the definitions and axioms satisfied by any solutions.

structure

(optional) specify the interpretation of some predicates, functions and constants.

The basic skeleton of an FO-dot knowledge base is as follows:

vocabulary {
    // here comes the specification of the vocabulary
}

theory {
    // here comes the definitions and axioms
}

structure {
    // here comes the interpretation of some symbols
}

Everything between // and the end of the line is a comment.

Shebang

New in version 0.5.5

The first line of an IDP-Z3 program may be a shebang line, specifying the version of IDP-Z3 to be used. When a version is specified, the Interactive Consultant and webIDE will be redirected to a server on the web running that version. The list of versions is available here. (The IDP-Z3 executable ignores the shebang.)

Example: #! IDP-Z3 0.5.4

Vocabulary

vocabulary V {
    // here comes the vocabulary named V
}

The vocabulary block specifies the types, predicates, functions and variables used to describe the problem domain. If the name is omitted, the vocabulary is named V.

Each declaration goes on a new line (or are space separated). Symbols begins with a word character excluding digits, followed by word characters. Word characters include alphabetic characters, digits, _, and unicode characters that can occur in words. Symbols can also be string literals delimited by ', e.g., 'blue planet'.

Types

IDP-Z3 supports built-in and custom types.

The built-in types are: 𝔹, , , Date, and Concept[signature] (where signature is any type signature, e.g. ()->Bool). The equivalent ASCII symbols are Bool, Int, and Real.

The type Concept[signature] has one constructor for each symbol (i.e., function, predicate or constant) declared in the vocabulary with that signature. The constructors are the names of the symbol, prefixed with `.

Custom types are declared using the keyword type, e.g., type color. Their name should be singular and capitalized, by convention.

Their extension can be defined in a structure, or directly in the vocabulary, by specifying:

  • a list of (ranges of) numeric literals, e.g., type someNumbers {0,1,2} or type byte {0..255} (the ASCII equivalent of is :=)

  • a list of (ranges of) dates, e.g., type dates {#2021-01-01, #2022-01-01} or type dates {#2021-01-01 .. #2022-01-01}

  • a list of nullary constructors, e.g., type Color {Red, Blue, Green}

  • a list of n-ary constructors; in that case, the enumeration must be preceded by constructed from, e.g., type Color2 constructed from {Red, Blue, Green, RGB(R: Byte, G: Byte, B: Byte)}

In the above example, the constructors of `Color are : Red, Blue, Green.

The constructors of `Color2 are : Red, Blue, Green and RGB. Each constructor have an associated function (e.g., is_Red, or is_RGB) to test if a Color2 term was created with that constructor. The RGB constructor takes 3 arguments of type Byte. R, G and B are accessor functions: when given a Color2 term constructed with RGB, they return the associated Byte. (When given a Color2 not constructed with RGB, they may raise an error)

Functions

The functions with name myFunc1, myFunc2, input domains p1, p2, p3 and output range p, are declared by:

myFunc1, myFunc2 : p1 ⨯ p2 ⨯ p3 → p

Their name should not start with a capital letter, by convention. The ASCII equivalent of is *, and of is ->.

The domains and ranges must be one of the following:

  • a previously-declared type

  • a previously-declared unary predicate

  • Concept[<signature>] to denote the set of concepts with a particular signature, e.g. Concept[Person -> Bool].

The functions must be total over their domain.

The type of each argument can be directly read in the signature when it is a type or set of concepts, or obtained by looking up the type of the argument of the unary predicate otherwise.

Predicates

A predicate is a function whose range is Bool.

A unary predicate is always interpreted as a subset of a type.

Variable Declarations

A variable may be declared with its type:

var x ∈ T

This is convenient for quantifications: the type of the variable may be omitted in quantifications: its declared type will be assumed.

A quantification cannot use a declared variable to quantify over another type than the declared one.

The variables x1, x2, ... are implicitly declared with the same type as x. (the variable in the declaration may not have a digital suffix)

Built-in functions

The following functions are built-in:

  • abs: Int Int (or abs: Float Float) yields the absolute value of an integer (or float) expression;

Propositions and Constants

A proposition is a predicate of arity 0; a constant is a function of arity 0.

MyProposition : () → 𝔹
MyConstant: () → Int

Include another vocabulary

A vocabulary W may include a previously defined vocabulary V:

vocabulary W {
    import V
    // here comes the vocabulary named W
}

Symbol annotations

To improve the display of functions and predicates in the Interactive Consultant, their declaration in the vocabulary can be annotated with their intended meaning, a short comment, or a long comment. These annotations are enclosed in [ and ], and come before the symbol declaration.

Intended meaning

[this is a text] specifies the intended meaning of the symbol. This text is shown in the header of the symbol’s box.

Short info

[short:this is a short comment] specifies the short comment of the symbol. This comment is shown when the mouse is over the info icon in the header of the symbol’s box.

Long info

[long:this is a long comment] specifies the long comment of the symbol. This comment is shown when the user clicks the info icon in the header of the symbol’s box.

English expression

[EN:{1} is a prime] specifies the English expression for prime: Int -> Bool. This information is used to generate the informal reading of a Theory. The number between brackets represents a placeholder for the English reading of the nth argument.

Slider

[slider: (a, b) in (0, 100)] displays as slider for a numeric value. The slider has a maximum range of [0, 100] that is reduced to [a(), b()] when the values of a() and b() are known (a and b are symbols in the vocabulary).

Theory

theory T:V {
    // here comes the theory named T, on vocabulary named V
}

A theory is a set of axioms and definitions to be satisfied, and of symbol interpretations. If the names are omitted, the theory is named T, for vocabulary V.

Symbol interpretations are described in the Section on Structure. Before explaining the syntax of axioms and definitions, we need to introduce the concept of term.

Mathematical expressions and Terms

A term is inductively defined as follows:

Boolean, Numeric and Date literals

true and false are boolean terms.

Numeric literals that follow the Python conventions are numerical terms of type Int or Real.

Date literals are terms. They follow ISO 8601 conventions, prefixed with # (i.e., #yyyy-mm-dd). #TODAY is also a Date literal representing today’s date. #TODAY(y, m, d) is a Date literal representing today shifted by y years, m months and d days, where y, m and d are integer literals (e.g., #TODAY(-18, 0, 0) is today 18 years ago).

Constructor

Each constructor of a type is a term having that type.

Variable

A variable is a term. Its type is derived from the quantifier expression that declares it (see below).

Function application

F(t_1, t_2,.., t_n) is a term, when F is a function symbol of arity n, and t_1, t_2,.., t_n are terms. Each term must be of the appropriate type, and in the domain of the function, as defined in the function declaration in the vocabulary. The resulting type and range of the function application is also defined in the function declaration. If the arity of F is 0, i.e., if F is a constant, then F() is a term.

Warning

The knowledge engineer must use appropriate if-then-else guards to ensure that the value of a function outside of its domain has no influence on the truth value of a statement.

For example: if y = 0 then 0 else x/y.

$(s)(t_1, t_2,.., t_n) is a term, when s is an expression of type Concept that denotes a function of arity n, and t_1, t_2,.., t_n are terms.

Please note that there are built-in functions (see Built-in functions).

Negation

-t is a numerical term, when t is a numerical term.

Arithmetic

t_1 t_2 is a numerical term, when t_1, t_2 are two numerical terms, and is one of the following math operators +, -, * (or ⨯), /, ^, %. Mathematical operators can be chained as customary (e.g. x+y+z). The usual order of binding is used.

Parenthesis

(t) is a term, when t is a term

Cardinality aggregate

#{v_1 in typeOfV_1, .., v_n in typeOfV_n : ϕ} is a numerical term when v_1  v_2 .. v_n are variables, and ϕ is a sentence containing these variables.

The term denotes the number of tuples of distinct values for v_1  v_2 .. v_n which make ϕ true.

Aggregate over anonymous function

agg(lambda v_1 in typeOfV_1, .., v_n in typeOfV_n : t) is a numerical term where agg can be any of (sum, min, max), v_1  v_2 .. v_n are variables and t is a term.

The term sum(lambda v in T : t(v)) denotes the sum of t(v) for each v in T. Similarly, min (resp. max) can be used to compute the minimum (resp. maximum) of t(v) for each v in T. t(v) can use the construct (if .. then .. else ..) to filter out unwanted v values.

(if .. then .. else ..)

(if t_1 then t_2 else t_3) is a term when t_1 is a formula, t_2 and t_3 are terms of the same type.

Sentences and axioms

An axiom is a sentence followed by .. A sentence is a well-formed formula without free variables (i.e., in which every variable appear in the scope of a quantifier that declares it). A formula is inductively defined as follows:

true and false

true and false are formulae.

Predicate application

P(t_1, t_2,.., t_n) is a formula, when P is a predicate symbol of arity n, and t_1, t_2,.., t_n are terms. Each term must be of the appropriate type, as defined in the predicate declaration. If the arity of P is 0, i.e., if P is a proposition, then P() is a formula.

$(s)(t_1, t_2,.., t_n) is a formula, when s is an expression of type Concept that denotes a predicate of arity n, and t_1, t_2,.., t_n are terms.

Comparison

t_1 t_2 is a formula, when t_1, t_2 are two numerical terms and is one of the following comparison operators <, ≤, =, ≥, >, (or, using ascii characters: =<, >=, ~=). Comparison operators can be chained as customary.

Negation

¬ϕ is a formula (or, using ascii characters: ) when ϕ is a formula.

Logic connectives

ϕ_1 ϕ_2 is a formula when ϕ_1, ϕ_2 are two formulae and is one of the following logic connectives ∨,∧,⇒,⇐,⇔ (or using ascii characters: |, \&, =>, <=, <=> respectively). Logic connectives can be chained as customary.

Parenthesis

(ϕ) is a formula when ϕ is a formula.

Enumeration

An enumeration (e.g. p := {1;2;3}) is a formula. Enumerations follow the syntax described in structure.

Quantified formulas

Quantified formulas are formulae. They have one of the following forms, where v_1, .., v_n are variables, p, p_1, .., p_n are types or predicates, and ϕ is a formula involving those variables:

∀ v_1, v_n: ϕ(v_1, v_n).

∀ v_1, v_n ∈ p: ϕ(v_1, v_n).

∀ (v_1, v_n) ∈ p: ϕ(v_1, v_n).

∀ v_1 ∈ p_1, v_n ∈ p_n: ϕ(v_1, v_n).

Alternatively, the existential quantifier, , can be used. Ascii characters can also be used: ?, !, respectively. For example, ! x, y in Int: f(x,y)=f(y,x).

A variable may only occur in the ϕ formula of a quantifier declaring that variable. In the first form above, the type of each variable is inferred from their declaration or from their use in ϕ.

“is enumerated”

f(a,b) is enumerated is a formula, where f is a function defined by an enumeration and applied to arguments a and b. Its truth value reflects whether (a,b) is enumerated in f’s enumeration. If the enumeration has a default value, every tuple of arguments is enumerated.

“in {1,2,3,4}”

f(args) in enum is a formula, where f is a function applied to arguments args and enum is an enumeration. This can also be written using Unicode: f() {1,2,3}.

if .. then .. else ..

if t_1 then t_2 else t_3 is a formula when t_1, t_2 and t_3 are formulae.

Definitions

A definition defines concepts, i.e. predicates or functions, in terms of other concepts. A definition consists of a set of rules, enclosed by { and }.

If a predicate is inductively defined in terms of itself, the definition employs the well-founded mode of interpretation by default. The other possible modes of interpretation are completion, Kripke-Kleene and co-induction. They can be selected by placing the keyword in parenthesis at the beginning of the definition, e.g., { (completion) ...}.

Rules have one of the following forms:

∀ v_1 ∈ T_1, v_n ∈ T_n: P(t_1, .., t_n) ← |phi|.

∀ v_1 ∈ T_1, v_n ∈ T_n: F(t_1, .., t_n) = t ← |phi|.

where P is a predicate symbol, F is a function symbol, t, t_1, t_2,.., t_n are terms that may contain the variables v_1  v_2 .. v_n and ϕ is a formula that may contain these variables. P(t_1, t_2,.., t_n) is called the head of the rule and ϕ the body. <- can be used instead of , and instead of =. If the body is true, the left arrow and body of the rule can be omitted.

Annotations

Some expressions can be annotated with their informal meaning, between brackets. For example, [age is a positive number] 0 =< age(). Such annotations are used in the Interactive Consultant.

The following expressions can be annotated:

  • Definitions

  • Rules

  • Constraints

  • Quantified formula

  • Comparisons

  • Membership in an enumeration

  • Brackets

When necessary, use parenthesis to avoid ambiguity, e.g. [Positive or p] ( [Positive] x()<0 ) | p()..

Structure

structure S:V {
    // here comes the structure named S, for vocabulary named V
}

A structure specifies the interpretation of some type, predicates and functions. If the names are omitted, the structure is named S, for vocabulary V.

A structure is a set of symbol interpretations of the form :

  • <symbol> <total interpretation>., e.g., P {1..9},

  • <symbol> <partial interpretation>., e.g., P {A->1}.

(The ASCII equivalent of is :=, and of is >>)

A total interpretation fully specifies the interpretation of the symbol; a partial interpretation does not.

An error occurs when the domain of the symbol is already known by enumeration, and its total interpretation does not cover the domain. If the domain of the symbol is not known, it is inferred from the total interpretation.

A total interpretation takes one of these forms:

for nullary predicates (propositions)

true or false

for non-numeric types and unary predicates:

a set of rigid terms (numbers, dates, identifiers, or constructors applied to rigid terms), e.g., {red, blue, green}.

for numeric types and unary predicates:

a set of numeric literals and ranges, e.g., {0,1,2}, {0..255} or {0..9, 90..99}

for date types and unary predicates:

a set of date literals and ranges, e.g., {#2021-01-01, #2022-01-01} or {#2021-01-01 .. #2022-01-01}

for types:

a set of n-ary constructors, preceded by constructed from, e.g., constructed from {Red, Blue, Green, RGB(R: Byte, G: Byte, B: Byte)} (see more details in types)

for n-ary predicates:

a set of tuples of rigid terms, e.g., {(a,b), (a,c)}.

for nullary functions:

a rigid term, e.g. 5 or #2021-01-01, or red or rgb(0,0,0)

for n-ary functions:

a set of tuples and their associated values, e.g., { (1,2)->3, (4, 5)->6 }. The interpretation may be followed by else <default>, where <default> is a default value (a rigid term), i.e., a value for the non-enumerated tuples, if any.

A partial interpretation takes one of these forms:

for n-ary functions:

a set of tuples and their associated values, e.g., { (1,2)->3, (4, 5)->6 }

Additional notes:

  • the set of tuples in the interpretation of a predicate is exactly the set of tuples that make the predicate true; any other tuple makes it false.

  • parenthesis around a tuple can be omitted when the arity is 1, e.g., {1-2, 3->4}

  • the interpretation of a predicate may be specified using the CSV format, with one tuple per line, e.g., :

P := {
1 2
3 4
5 6
}
  • The interpretation of goal_string is used to compute relevance relative to goals (see the determine_relevance method in the Theory class).

  • The tuples of an interpretation can be given in any order.

Differences with IDP3

Here are the main differences with IDP3 (the previous version of IDP-Z3), listed for migration purposes:

Infinite domains

IDP-Z3 supports infinite domains: Int, Real. However, quantifications over infinite domains is discouraged.

Type

IDP-Z3 supports type hierarchies differently from IDP3: subtypes are now represented by unary predicates; unary predicates can be used wherever types can be used, i.e., in type signatures and in quantifiers.

LTC

IDP-Z3 does not support LTC vocabularies.

Namespaces

IDP-Z3 does not support namespaces.

Partial functions

In IDP-Z3, a function must be total over a cross-product of (sub-)types. The handling of division by 0 may differ. See IEP 07

Syntax changes

The syntax of quantifications and aggregates has slightly change. IDP-Z3 does not support qualified quantifications, e.g. !2 x[color]: p(x).. (p. 11 of the IDP3 manual). Such statements can be implemented in IDP-Z3 using cardinality constraints instead.

if .. then .. else ..

IDP-Z3 supports if .. then .. else .. terms and sentences.

Structure

IDP-Z3 supports partial interpretations of functions using the >> sign. (It currently does not support partial interpretations of predicates)

Procedure blocks

IDP-Z3 only recognizes the main() block, written in Python (instead of in Lua).

To improve performance, do not quantify over the value of a function. Use p(f(x)) instead of ?y: f(x)=y & p(y).