The FO[·] Language¶
Overview¶
The FO[·] (aka FOdot) language is used to create knowledge bases. It is described in the FOdot standard. This document presents the implementation in IDPZ3.
An FOdot 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 FOdot 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 IDPZ3 program may be a shebang line, specifying the version of IDPZ3 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 IDPZ3 executable ignores the shebang.)
Example: #! IDPZ3 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¶
IDPZ3 supports builtin and custom types and subtypes.
The builtin 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 type signature.
The constructors are the names of the symbol, prefixed with `
.
Custom types are declared using one of these templates:
type T
type T ≜ {<an enumeration>}
type T ⊆ T1
type T ≜ {<an enumeration>} ⊆ T1
where T1
is a previously declared type.
The third and fourth declarations say that T
is a subtype of T1
, i.e., that its interpretation is a subset of the interpretation of T1
.
The name of types should be singular and capitalized, by convention.
The ASCII equivalent of ⊆
is <:
.
The extension of a type must 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}
ortype byte ≜ {0..255}
(the ASCII equivalent of≜
is:=
)a list of (ranges of) dates, e.g.,
type dates ≜ {#20210101, #20220101}
ortype dates ≜ {#20210101 .. #20220101}
a list of nullary constructors, e.g.,
type Color ≜ {Red, Blue, Green}
a list of nary 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)
 Constructors can be used to construct recursive datatypes ,
e.g.,
type List := constructed from {nil, cons(car:Color, cdr: List)}
.
(However, unsatisfiable theories with recursive definitions do not terminate; propagation and explanation inferences are not supported).
Predicates¶
A predicate is declared using one of these templates:
p : T1⨯..⨯Tn → 𝔹
where T1,..,Tn
are previously declared types.
The declaration says that p
takes arguments of type T1⨯ .. ⨯Tn
.
The predicate names should start with a lowercase letter, by convention.
The ASCII equivalent of ⨯
is *
, of →
is >
and of ⊆
is <:
.
A unary predicate is always interpreted as a subset of a type. A nullary predicate is a subset of the singleton set containing the empty tuple.
Functions¶
A function is declared using one of these templates:
f : total T1⨯..⨯Tn → T
f : T1⨯..⨯Tn → T (domain: p1⨯..⨯pn, codomain: q)
f : T1⨯..⨯Tn → T (domain: p, codomain: q)
f : partial T1⨯..⨯Tn → T
where T1,..,Tn, T
are previously declared types and p, p1,.., pn, q
are previouslydeclared types or predicates.
All 4 declarations say that f
takes arguments of type T1⨯..⨯Tn
.
The first declaration says that f
is a total function.
The total
keyword is optional but recommended.
The second declaration says that f
is defined over exactly the crossproducts of the sets p1⨯..⨯pn
, and that its image is a subset of q
(T > Bool
).
The third declaration says that f
is defined over exactly p
(with type signature T1⨯..⨯Tn > Bool
), and that its image is a subset of q
(T > Bool
).
The fourth declaration says that f
is defined over exactly dom_f
, where dom_f
is an implicitly declared predicate with type signature T1*..*Tn > Bool
.
The domain
(resp. codomain
) specifies the domain of definition (resp. the codomain) of the function.
It can be omitted when it is T1⨯..⨯Tn
(resp. T
), but must be given otherwise.
The function names should start with a lowercase letter, by convention.
The ASCII equivalent of ⨯
is *
, and of →
is >
.
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)
Builtin functions¶
The following functions are builtin:
abs: Int → Int
(orabs: 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 forprime: 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
andb
are symbols in the vocabulary).
URIs¶
New in version 0.11.1
IDPZ3 has support for URIs in virtually every place where you can write a string: block names, symbol names, names of type elements and constructor names. The only exception are variable names, which cannot be written using a URI.
There are a number of reasons for introducing URIs in your FO(·) specification, but the main benefit is providing a simple way to refer to “external concepts”. Additionally, it offers improved interoperability with knowledge graph technologies.
The syntax of URIs in FO(·) aims to stay as close as possible to that of the commonly used RDF standard. An example of a vocabulary declaration with absolute URIs is as follows:
vocabulary V {
type <http://www.example.org/whatever#Type>
type Whatever
<http://www.example.org/whatever#foo>: <http://www.example.org/whatever#Type> > Bool
bar: Whatever > <http://www.example.org/whatever#Type>
<http://www.example.org/whatever#Somethingelse>: > Int
}
To prevent lengthy names, you may also shorten your URIs by introducing a prefix.
The syntax to declare the prefix is as follows: @prefix: *name* <https://www.your.uri/something#>.
.
It must either be declared at the top of the file, in which case it is valid to use everywhere in the FO(·) specification, or at the top of a vocabulary block, in which case you may only use it inside that vocabulary and all blocks that inherit it.
The syntax to use the prefix is we::foo
, which is equivalent to <http://www.example.org/whatever#foo>
.
As an example:
@prefix we: <http://www.example.org/whatever#>.
vocabulary V {
type we::Type
we::bar: () > we::Type
}
Note
Internally, IDPZ3 will not expand prefixed URIs to absolute URIs, meaning that IDPZ3 will regard the same concept expressed using an absolute and prefixed URI differently: e.g., we::foo ~= <http://wwww.example.org/whatever#foo>
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
andfalse
are boolean terms.Numeric literals that follow the Python conventions are numerical terms of type
Int
orReal
.Date literals are terms. They follow ISO 8601 conventions, prefixed with
#
(i.e.,#yyyymmdd
).#TODAY
is also a Date literal representing today’s date.#TODAY(y, m, d)
is a Date literal representing today shifted byy
years,m
months andd
days, wherey
,m
andd
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, whenF
is a function symbol of arityn
, andt_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 ofF
is 0, i.e., ifF
is a constant, thenF()
is a term.Warning
The knowledge engineer must use appropriate ifthenelse 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, whens
is an expression of type Concept that denotes a function of arityn
, andt_1, t_2,.., t_n
are terms.Please note that there are builtin functions (see Builtin functions).
 Negation

t
is a numerical term, whent
is a numerical term. Arithmetic
t_1 ꕕ t_2
is a numerical term, whent_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, whent
is a term Cardinality aggregate
#{v_1 in typeOfV_1, .., v_n in typeOfV_n : ϕ}
is a numerical term whenv_1 v_2 .. v_n
are variables, andϕ
is a sentence containing these variables. If: ϕ
is omitted,ϕ
is presumed to betrue
.The term denotes the number of tuples of distinct values for
v_1 v_2 .. v_n
which makeϕ
true. Aggregate over sets
agg{ t  v_1 in typeOfV_1, .., v_n in typeOfV_n : p}
is a numerical term whereagg
can bemin
ormax
,v_1 v_2 .. v_n
are variables,t
is a term andp
is a boolean expression. The variables declared by the aggregate can occur int
andp
. If: p
is omitted,p
is presumed to betrue
.This aggregate denotes the minimum (resp. maximum) of term
t
for each value of the variables that satisfiesp
. Note that the set must be nonempty. Aggregate over multisets
The term
agg{{ t  v_1 in typeOfV_1, .., v_n in typeOfV_n : p}}
whereagg
can besum
,min
ormax
, denotes the aggregate of the termt
for each value of the variables that satisfies boolean expressionp
. The variables declared by the aggregate can occur int
andp
. If: p
is omitted,p
is presumed to betrue
. Note that the set must be nonempty, or the aggregate must be ``sum’’. (if .. then .. else ..)
(if t_1 then t_2 else t_3)
is a term whent_1
is a formula,t_2
andt_3
are terms of the same type.
Sentences and axioms¶
An axiom is a sentence followed by .
.
A sentence is a wellformed 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
andfalse
are formulae.
 Predicate application
P(t_1, t_2,.., t_n)
is a formula, whenP
is a predicate symbol of arityn
, andt_1, t_2,.., t_n
are terms. Each term must be of the appropriate type, as defined in the predicate declaration. If the arity ofP
is 0, i.e., ifP
is a proposition, thenP()
is a formula.$(s)(t_1, t_2,.., t_n)
is a formula, whens
is an expression of type Concept that denotes a predicate of arityn
, andt_1, t_2,.., t_n
are terms. Comparison
t_1 ꕕ t_2
is a formula, whent_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.Connectives can be written in English, e.g.
and
. See full list of English connectives in Syntax summary. Parenthesis
(
ϕ
) is a formula whenϕ
is a formula.
 Enumeration
An enumeration (e.g.
p := {1,2,3}
) is a formula. An enumeration must be toplevel (i.e., an assertion in a theory) 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 variables must have been declared (without any numeric suffix) in the vocabulary. “is enumerated”
f(a,b) is enumerated
is a formula, wheref
is a function defined by a (partial) enumeration and applied to argumentsa
andb
. Its truth value reflects whether(a,b)
is enumerated inf
’s (partial) 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, wheref
is a function applied to argumentsargs
andenum
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 whent_1
,t_2
andt_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 wellfounded mode of interpretation by default.
The other possible modes of interpretation are completion
, KripkeKleene
,
coinduction
, stable'' and ``recursive
(for recursive datatypes).
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
orfalse
 for nonnumeric 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.,
{#20210101, #20220101}
or{#20210101 .. #20220101}
 for types:
a set of nary 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 nary predicates:
a set of tuples of rigid terms, e.g.,
{(a,b), (a,c)}
. for nullary functions:
a rigid term, e.g.
5
or#20210101
, orred
orrgb(0,0,0)
 for nary functions:
a set of tuples and their associated values, e.g.,
{ (1,2)>3, (4, 5)>6 }
. The interpretation may be followed byelse <default>
, where<default>
is a default value (a rigid term), i.e., a value for the nonenumerated tuples, if any.
A partial interpretation takes one of these forms:
 for nary 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.,
{12, 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 thedetermine_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 IDPZ3), listed for migration purposes:
 Infinite domains
IDPZ3 supports infinite domains:
Int, Real
. However, quantifications over infinite domains is discouraged. Type
IDPZ3 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
IDPZ3 does not support LTC vocabularies.
 Namespaces
IDPZ3 does not support namespaces.
 Partial functions
The handling of division by 0 may differ. See IEP 07
 Syntax changes
The syntax of quantifications and aggregates has slightly change. IDPZ3 does not support qualified quantifications, e.g.
!2 x[color]: p(x).
. (p. 11 of the IDP3 manual). Such statements can be implemented in IDPZ3 using cardinality constraints instead. if .. then .. else ..
IDPZ3 supports if .. then .. else .. terms and sentences.
 Structure
IDPZ3 supports partial interpretations of functions using the :> sign. (It currently does not support partial interpretations of predicates)
 Procedure blocks
IDPZ3 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)
.