Idp3 Manual
User Manual:
Open the PDF directly: View PDF 
.
Page Count: 29
The IDP framework reference manual
KU Leuven Knowledge Representation and Reasoning research group
September 25, 2015
1
Contents
1 Installing And Running 4
1.1 Gettingthesystem..................................... 4
1.1.1 Downloading the most recent version . . . . . . . . . . . . . . . . . . . . . . . 4
1.1.2 Buildingfromsource................................ 4
1.2 Runningthesoftware.................................... 4
1.2.1 Batchmode..................................... 4
1.2.2 Interactivemode .................................. 5
2 Comments 5
3 Include statements 5
4 Namespaces 5
5 Vocabularies 6
5.1 Symboldeclarations .................................... 6
5.2 Symbolpointers ...................................... 7
5.3 Thestandardvocabulary ................................. 8
5.4 LTCvocabularies...................................... 9
6 Theories 9
6.1 Sentences .......................................... 10
6.1.1 Terms ........................................ 10
6.1.2 Formulas and Sentences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
6.1.3 Definitions ..................................... 11
6.2 Chainsof(in)equalities................................... 12
6.3 Aggregates ......................................... 12
6.3.1 Aggregates on lists of terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
6.3.2 Aggregates on lists of formulas . . . . . . . . . . . . . . . . . . . . . . . . . . 13
6.4 Partialfunctions ...................................... 13
6.5 TheTypeofaVariable .................................. 14
6.5.1 Automatic derivation of types for variables . . . . . . . . . . . . . . . . . . . 14
7 Terms 15
8 Queries 15
9 Structures 15
9.1 Contentsofastructure................................... 15
9.1.1 TypeEnumeration................................. 16
9.1.2 Predicate Enumeration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
9.1.3 FunctionEnumeration............................... 16
9.1.4 Three-Valued Predicate/Function interpretations . . . . . . . . . . . . . . . . 17
9.1.5 Interpretation by Procedures . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
9.1.6 Shorthands ..................................... 17
9.2 factlist............................................ 17
2
10 Procedures 17
10.1Declaringaprocedure ................................... 17
10.2 IDP types.......................................... 18
10.3Built-inprocedures..................................... 19
10.3.1 stdspace....................................... 19
10.3.2 idpintern ...................................... 19
10.3.3 inferences ...................................... 20
10.3.4 options ....................................... 22
10.3.5 structure ...................................... 23
10.3.6 theory........................................ 24
10.3.7 vocabulary ..................................... 24
10.3.8 Miscellaneous.................................... 25
10.3.9 The table_utils library . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
11 Options 25
11.1Verbosityoptions...................................... 25
11.2Modelexpansionoptions .................................. 26
11.3Propagationoptions .................................... 27
11.4Printingoptions ...................................... 27
11.5Entailmentoptions..................................... 27
11.6Generaloptions....................................... 27
12 IDP2vs IDP328
13 Common errors and warnings 29
13.1Syntaxerror......................................... 29
13.2Unquantifiedvariables ................................... 29
13.3Derivedtype ........................................ 29
13.4Underivabletype ...................................... 29
13.5Infinitegrounding...................................... 29
3
1 Installing And Running
The system has been verified to run under Windows and various Unix versions. The system also
works under OSX, but for any version at or below Lion it requires developer components on the
user machine to run.
1.1 Getting the system
1.1.1 Downloading the most recent version
Pre-built binaries can be retrieved from http://dtai.cs.kuleuven.be/krr/software/idp and
installed in their default (OS-specific) way. For the reasons stated above, we do not provide pre-
built OSX packages.
1.1.2 Building from source
Required software packages:
•C and C++ compiler, supporting most of the C++11 standard. Examples are GCC 4.4,
Clang 3.1 and Visual Studio 11 or higher.
•Cmake build environment.
•Bison and Flex parser generator software.
•Pdflatex for building the documentation.
Assume idp is unpacked in idpdir, you want to build in builddir (cannot be the same as
idpdir) and install in installdir. Building and installing is then achieved by executing the
following commands:
cd <b u i l d d i r >
cmake <i d p d i r > −DCMAKE_INSTALL_PREFIX=<i n s t a l l d i r >
−DCMAKE_BUILD_TYPE=" R e l ea s e "
make −j 4
make check
make i n s t a l l
Alternatively, cmake-gui can be used as a graphical way to set cmake options.
1.2 Running the software
1.2.1 Batch mode
One-shot execution of a procedure proc with a set of files files is achieved by running
id p −e " proc ( ) " f i l e s
Omitting the -e option results in execution of the main method if any is available.
4
1.2.2 Interactive mode
An interactive session, with (optionally) a set of files files, is started with
id p f i l e s −i
Afterwards, help can be requested with the help() command. Auto-completion of available
commands is available via the tab key. Additional files can be included with the parse command.
2 Comments
Everything between /* and */ is a comment, as well as everything between // and the end of the
line. If a comment block starts with /**, but not with /***, then the comment is added as a
description to the first thing after that comment block that can have a description. Currently, only
procedures can have a description.
3 Include statements
Everywhere in an IDP file at location dir, a statement
include " path / to / f i l e "
is replaced by the contents of dir/path/to/file or path/to/file if the first one does not exists.
If none exist, an error is thrown. Every file can only be included once; if it is included more often, it
will be ignored the second time. However, if you include a file multiple times in different ways (by
using different symbol links for example), we might not detect that it is the same file, and include
it more than once. We discourage this behavior.
A statement
include <f il ena me >
is replaced by the contents of the standard library file filename. Currently the following standard
library files are available:
mx Contains some useful model expansion procedures.
table_utils Contains tools for manipulating tables and converting IDP tables to lua tables.
4 Namespaces
A namespace with name MySpace is declared by
namespace MySpace {
// co n te n t o f th e namespace
}
A Namespace can contain namespaces, vocabularies, theories, structures, terms, queries, proce-
dures, options and using statements.
5
An object with name MyName declared in namespace MySpace can be referred to by absolute
qualification: MySpace::MyName. Inside MySpace,MyName can simply be referred to by MyName.
Additionally, using statements can be used to allow relative qualification. A using statement is of
one of the following forms
using namespace MySpace
using vocabulary MyVoc
where MySpace is the name of a namespace, and MyVoc the name of a vocabulary. Below such
a using statement, objects MyObj declared in MySpace, respectively MyVoc, can be referred to by
MyObj, instead of MySpace::Myobj, respectively MyVoc::MyObj.
Every object that is declared outside a namespace, is considered to be part of the global
namespace, called idpglobal. In other words, every IDP file implicitely starts with namespace
idpglobal{ and ends with an additional }. Everything declared inside a library is contained within
the namespace stdspace. It is discouraged to add or overwrite objects within stdspace.
5 Vocabularies
A vocabulary with name MyVoc is declared by
vocabulary MyVoc {
// c o n t e n t s o f t h e v o c ab u la r y
}
A vocabulary can contain symbol declarations, symbol pointers, and other vocabularies. Symbols
are types (sorts), predicate and functions symbols.
5.1 Symbol declarations
A type with name MyType is declared by
type MyType
When declaring a type, it can be stated that this type is a subtype or supertype of a set of other
types. The following declares MyType to be a subtype of the previously declared types A1 and A2,
and a supertype of the previously declared types B1 and B2:
type MyType isa A1 , A2 contains B1 , B2
In the rest of this text, we will sometimes use “parent type” as direct supertype and “ancestor type”
for (in)direct supertype.
Types can also be constructed using the constructed from keywords. A constructed type has
a fixed interpretation which is the union of the images of a set of constructor functions. These
constructor functions each have an interpretation which maps every tuple from their domain to a
unique domain element in the interpretation of the constructed type. Constructor functions should
not be explicitly declared by the vocabulary; a function occurring in the declaration is automatically
declared as a constructor function. E.g., a constructed type Square with constructors Index/2 and
SpecialSquare/0 is declared as by
6
type T1
type Square constructed from { P o s i t i o n (T1 , T1 ) , S p e c i a l S q u a r e }
Note that constructed types currently do not support any type inheritance.
Also note that it is impossible to construct numerical types, since numerals simply are not
constructor functions. However, sometimes it is useful to interpret a numerical type independent
of any structure. This can be done in the vocabulary with a similar syntax as when the type would
be interpreted in a structure. It is possible to make such a type inherit from a numerical supertype,
or make it contain a numerical subtype.
type SmallPrimes = { 2 ; 3 ; 5 ; 7 } isa nat
A predicate with name MyPred, arity 3 and types T1,T2,T3 is declared by
MyPred (T1 , T2 , T3)
A predicate with arity zero can be declared by MyPred() or MyPred.
A function with name MyFunc, input types T1,T2,T3 and output type Tis declared by
MyFunc(T1 , T2 , T3 ) : T
A partial function is declared by
partial MyFunc(T1 , T2 , T3 ) : T
Constants of type Tcan be declared by MyConst:T or MyConst():T.
Any symbol has to be declared on its own line.
Invalid symbol names are: isa, type, extends, contains, extern
5.2 Symbol pointers
To include a type, predicate, or function from a previously declared vocabulary Vin another vo-
cabulary W, write
/∗D e c l a r a t i o n o f vo c ab u la r y V∗/
vocabulary V {
// . . .
type A
P(A)
F(A,A) : A
// . . .
}
vocabulary W {
extern type V : : A
extern V : : P [A] // a l s o p o s s i b l e : e xt ern V : : P/1
extern V : : F [ A,A :A] // a l s o p o s s i b l e : e xt ern V : : F/2 :1
}
7
In the example, explicitly including type Aof vocabulary Vin Wis not needed, since types
of included predicates or functions are automatically included themselves. To include the whole
vocabulary Vin Wat once, used
vocabulary W {
extern vocabulary V
}
5.3 The standard vocabulary
The global namespace contains a fixed vocabulary std, which is defined as follows:
vocabulary std {
type nat
type int contains nat
+(int ,int ) : int
−(int ,int) : int
∗(int ,int) : int
partial /( int ,int ) : int
%(int ,int ) : int
abs ( int) : int
−(int) : int
}
Every vocabulary implicitly contains all symbols of std. Also, every vocabulary contains for each of
its types Athe predicates =(A,A),<(A,A), and >(A,A) and the functions MIN:A,MAX:A,SUCC(A):A
and PRED(A):A. In every structure, the symbols of std have the following interpretation:
nat all natural numbers
int all integer numbers
+(int,int) : int integer addition
-(int,int) : int integer subtraction
*(int,int) : int integer multiplication
/(int,int) : int division (only defined when the second argument is a non-zero divisor of the first)
%(int,int) : int remainder
abs(int) : int absolute value
-(int) : int unary minus
The predicate =/2 is always interpreted by equality. The order <dom on domain elements is
defined by
•numbers are smaller than non-numbers;
•d1<dom d2if d1and d2are numbers and d1< d2;
•d1<dom d2if d1and d2are strings that are not numbers and d1is before d2in the lexicographic
ordering;
8
•d1<dom d2is some total order on compound domain elements (which we do not specify).
Every structure contains the following fixed interpretations:
<(A,A) the projection of <dom to the domain of A
>(A,A) the projection of >dom to the domain of A
MIN:A the <dom-least element in the domain of A
MAX:A the <dom-greatest element in the domain of A
SUCC(A):A the partial function that maps an element a of the domain of A
to the <dom-least element of the domain of A that is strictly larger than a
PRED(A):A the partial function that maps an element a of the domain of A
to the <dom-greatest element of the domain of A that is strictly smaller than a
In an IDP-file, you should disambiguate which MAX you want to use. This is done by MAX[:MyType].
5.4 LTC vocabularies
You can declare a vocabulary to be an LTC-vocabulary, as defined here. Thus, a vocabulary
containing a type T ime, a constant Start typed T ime and a function Next,T ime →T ime. If
these types and functions have the above name, you do this as follows
LTCvocabulary V {
type Time
S t a r t : Time
Next ( Time ) : Time
. . . // Re st o f you r v oc ab u la ry
}
Doing so automatically creates vocabularies V_ss (singlestate vocabulary) and V_bs (bistate
vocabulary).
In case your type T ime is called differently, you can inform IDP about this with:
LTCvocabulary V (MyTime , MyStart , MyNext ) {
type MyTime
MyStart : MyTime
MyNext(MyTime ) : MyTime
. . . // Re st o f you r v oc ab u la ry
}
6 Theories
A theory with name MyTheory over a vocabulary MyVoc is declared by
theory MyTheory : MyVoc {
// c o n t e n t s o f t h e t h e or y
}
A theory contains sentences and inductive definitions.
9
6.1 Sentences
6.1.1 Terms
Before explaining the syntax for sentences, we need to introduce the concept of a term and a for-
mula. We also give the syntax for terms and formulas in IDP.
Aterm is inductively defined as follows:
•a variable is a term;
•a constant is a term;
•if Fis a function symbol with ninput arguments and t1, . . . , tnare terms, then F(t1, . . . , tn)
is a term.
In IDP, variables start with a letter and may contain letters, digits and underscores. When writing a
term in IDP, the constant and function symbols occurring in that term should be declared before.
The type of a term is defined as its return type (see section 5.1) in the case of constants and
functions. The type of a variable is derived from its occurrences in formulas (see section 6.5). If a
term occurs in an input position of a function, then the type of the term and the type of the input
position must have a common ancestor type.
6.1.2 Formulas and Sentences
Aformula is inductively defined by:
•true and false are formulas;
•if Pis a predicate symbol with arity nand t1, . . . , tnare terms, then P(t1, . . . , tn)is a formula;
•if t1and t2are terms, then t1=t2is a formula;
•if ϕand ψare formulas and xis a variable, then the following are formulas: ¬ϕ,ϕ∧ψ,ϕ∨ψ,
ϕ⇒ψ,ϕ⇐ψ,ϕ⇔ψ,∀x ϕ, and ∃x ϕ.
The following order of binding is used: ¬binds tightest, next ∧, then ∨, then ⇐, followed by
⇒, then ⇔, and finally ∀and ∃. All operators are right associative, for example P⇒Q⇒Ris
equivalent to the formula P⇒(Q⇒R). Disambiguation can be done using brackets ‘(’ and ‘)’. E.g.
the formula ∀x P (x)∧ ¬Q(x)⇒R(x)is equivalent to the formula ∀x((P(x)∧(¬Q(x))) ⇒R(x)).
As for terms, if term toccurs in predicate P, then the type of tand the type of the input
position of Pwhere it occurs must have a common ancestor type. For formulas of the form t1=t2,
t1and t2must have a common ancestor type.
The scope of a quantification ∀xor ∃x, is the quantified formula. E.g., in ∀x ψ, the scope of ∀x
is the formula ψ. An occurrence of a variable xthat is not inside the scope of a quantification ∀x
or ∃xis called free. A sentence is a formula containing no free occurrences of variables. If an IDP
problem specification contains formulas that are not sentences, the system will implicitly quantify
this variable universally and return a warning message, specifying which variables occur free. Each
sentence in IDP ends with a dot ‘.’.
The IDP syntax of the different symbols in formulas are given in the table below. Also the
informal meaning of the symbols is given.
10
Logic IDP Declarative reading
∧&and
∨|or
¬ ∼ not
⇒=> implies
⇐<= is implied by
⇔<=> is equivalent to
∀!for each
∃?there exists
==equals
6=∼=does not equal
Besides this, for every natural number n,IDP also supports the following quantifiers (with their
respective meanings):
IDP Declarative reading
?n there exist exactly ndifferent elements such that
?<n there exist less than n
?=<n there exist at most n
?=n there exist exactly n(this is the same as ?n)
?>n there exist more than n
A universally quantified formula ∀x P (x)becomes ‘! x : P(x)’ in IDP syntax, and similarly for
existentially quantified formulas. As a shorthand for the formula ‘! x : ! y : ! z : Q(x,y,z).’, one
can write ‘! x y z : Q(x,y,z)’.
IDP also supports binary quantifications, which allow to writer shorter or more readable for-
mulas:
Binary Quantification Shorthand for
? (x,y) in P : Q(x,y) ? x y : P(x,y) & Q(x,y)
! (x,y) in P : Q(x,y) ! x y : P(x,y) => Q(x,y)
? (x,y) sat P(x,y) : Q(x,y) ? x y : P(x,y) & Q(x,y)
! (x,y) sat P(x,y) : Q(x,y) ! x y : P(x,y) => Q(x,y)
In IDP, every variable has a type. The informal meaning of a sentence of the form ∀x ψ,
respectively ∃x ψ, where xhas type Tis then ‘for each object xof type T,ψmust be true’,
respectively ‘there exists at least one object xof type Tsuch that ψis true’. The type of a variable
can be declared by the user, or derived by IDP (see section 6.5).
6.1.3 Definitions
A definition defines a concept, i.e. a predicate (or multiple predicates), in terms of other predicates.
Formally, a definition is a set of rules of the form
∀x1, . . . , xnP(t1, . . . , tm)←ϕ
where Pis a predicate symbol, t1, . . . , tmare terms that may contain the variables x1, . . . , xnand
ϕa formula that may contain these variables. P(t1, . . . , tm)is called the head of the rule and ψthe
body.
11
A definition in IDP syntax consists of a set of rules, enclosed by ‘{’ and ‘}’. Each rule ends with
a ‘.’. The definitional implication ←is written ‘<-’. The quantifications before the head may be
omitted in IDP (IDP will give a warning in this case), i.e., all free variables of a rule are implicitly
universally quantified. If the body of a rule is empty (true), the rule symbol ‘<-’ can be omitted.
Recursive definitions are allowed in IDP. The semantics for a definitions are the well-founded
semantics . As an example, the following definition defines the transitive closure of a relation R.
{
! x y : T( x , y ) <−R( x , y ) .
! x y : T( x , y ) <−? z : T( x , z ) & T( z , y ) .
}
6.2 Chains of (in)equalities
As in mathematics, one can write chains of (in)equalities in IDP. They can be used as shorthands
for conjunctions of (in)equalities. E.g.:
! x y : ( 1 =< x < y =< 5) => . . .
// i s a shorthand f o r
! x y : ( ( 1 =< x ) & ( x < y ) & ( y =< 5 ) ) => . . .
6.3 Aggregates
Aggregates are functions that take a set as argument, instead of a simple variable. IDP supports
some aggregates that map a set to an integer. As such, they can be seen as integer terms.
Syntacticly, one writes sets in IDP in the following manner:
•An expression of the form ‘{ x_1 x_2 ... x_n : phi : t}’, where the x_i are variables,
phi is a formula and tis a term. The variables x_i can occur in both phi and t.
The informal interpretation of sets is:
•The multiset consisting of: for every tuple of domain elements (a_1,a_2, ...,a_n), the
term t[a_i/x_i] if phi[a_i/x_i] is true.
The current system has support for five aggregate functions:
Cardinality: The cardinality of a set is the number of elements in that set. The IDP syntax
for the cardinality of a set Sis ‘card S’ or ‘#S’ and this denotes the number of tuples
(a_1,a_2,..., a_n) such that phi is true.
Sum: Let Sbe a set of the form, i.e., of the form ‘{ x_1 x_2 ... x_n : phi : t }’. Then
the interpretation of ‘sum S’ denotes the number
X
(a_1,a_2,...,a_n)|Iphi
t,
i.e., it is the sum of all the terms for which there exist a_1,..., a_n that make the formula
phi true. For sets of the first sort, this is interpreted as
X
i|Iphi_i
ti.
12
Product: Products are defined similarly to sum. The syntax for the product of Sis prod S.
Maximum: One can write ‘max S’ to denote the maximum value of the terms in S, i.e.,
max
(a_1,a_2,...,a_n)|Iphi
t
for sets of the second sort. Sets of the first sort are handled analogously.
Minimum: To get the minimum value, write ‘min S’.
When using cardinality, the terms do not matter. You can choose to write 1for every term, but
are also allowed to leave out the terms.
6.3.1 Aggregates on lists of terms
Next to these aggregates that take a set as argument, IDP also supports lists of terms as a set.
IDP supports four operations in this syntax: Sum, Max, Min and Prod. A sum operation would
look like this:
sum(t1, t2, t3, . . . , tn)
and is interpreted as
X
i=1..n
ti
The three other operations are similar.
6.3.2 Aggregates on lists of formulas
For the fifth aggregate Card, IDP supports lists of formulas. A formula with cardinality aggregate
on list looks like this:
∀x: (#(F1(x), F2(x), . . . , Fk(x)) = n)
This means that for every xexactly nformulas in that list are true. For example,
∀x[F igure] : (#(T riangle(x), Square(x), P entagon(x)) = 1)
means that every figure is Triangle, Square or Pentagon, but never both or all three of them.
6.4 Partial functions
Normally, functions are total: they assign an output value to each of the input values. On the
other hand, partial functions do not necessarily have this property. In IDP, a partial function F
can arise in different situations. Either Fis explicitly declared as partial, or it is a built-in integer
function (for example modulo).
The semantics of a partial function Fis given by transforming constraints and rules where F
occurs as follows:
•in a positive context, P(...,F(x), . . .)is transformed to ∀y(F(x) = y⇒P(...,y,...));
•in a negative context, P(...,F(x), . . .)is transformed to ∃y(F(y) = y∧P(...,y,...)).
Here, P(...,F(x), . . .)occurs in a positive context if it occurs in sentence and in the scope of an
even number of negations, or it occurs in a body of a rule and in the scope of an odd number of
negations. All other occurrences are in a negative context.
13
6.5 The Type of a Variable
There are two ways to assign a type tto a variable v:
•Explicitly mention the type of vbetween ‘[’ and ‘]’ when vis quantified. Then vgets type t
in the scope of the quantifier. E.g.,
theory T: V {
! MyVar [ MyType ] : ? MyVar2 [ MyType2 ] MyVar3 [ MyType3 ] : // . . .
}
•Do not mention the type of vbut let the system automatically derive it. The rest of this
section explains how this is done.
6.5.1 Automatic derivation of types for variables
We distinguish between typed and untyped occurrences. The following are typed occurrences of a
variable x:
•an occurrence as argument of a non-overloaded predicate: P(...,x,...);
•an occurrence as argument of a non-overloaded function: F(...,x,...) = . . .;
•an occurrence as return value of a non-overloaded function: F(. . .) = xor F(. . .)6=x.
All others positions are untyped.
An overloaded predicate or function symbol can be disambiguated by specifying its vocabulary
and/or types. E.g.,
! x : MyVoc : : P [ A,A] ( x , x ) .
! y : ?1 x : F [A:A] ( x ) = y .
MyVoc : : C [ : A] > 2 .
In this case, the occurrences of all variables are typed.
Basically, if a variable occurs in one typed position, it gets the type of that position. If a declared
variable with type T_1 occurs in a typed position of type T_2, then T_1 and T_2 should have a
common ancestor type.
The more complicated cases arise when a variable does not occur in any typed position, or it
occurs in two typed positions with a different type. The system is designed to give a reasonable
type to such variables. However, the choices made by the system might be ad hoc or not the ones
the user intended, hence, every time IDP derives a type, it will give a warning, including which
type it derived for the variable.
First consider the case where a variable occurs in typed positions with different types. If all
the typed positions where the variable occurs have a common ancestor type T, then the variable
is assigned the least common ancestor of those types. If they do not have a common ancestor, no
derivation is done.
Now consider the case where a variable does not occur in a typed position. Then, the IDP
system tries to find out what the type of the variable should be using its occurrences in untyped
positions in built-in overloaded functions. For example, when a variable xonly occurs in x=t,
then xwill get the same type as t. It’s always safer to declare a type for the variable in this case.
If it is not possible to derive a type for xin this way either, the IDP system reports an error.
14
7 Terms
Besides from appearing in theories, terms can also be defined separately, for example for use in a
minimize inference. The syntax for declaring a term MyTerm over a vocabulary MyVoc is
term MyStruct : MyVoc {
// c o n t e n t s o f t he term
}
8 Queries
A query with name MyQuery over a vocabulary MyVoc is declared by
query MyQuery : MyVoc {
// c o n t e n t s o f t he qu er y
}
Here “contents of the query” is of the following form
{ MyVar1 MyVar2 . . . MyVarn : MyFormula}
where all free variables of the FO(·)formula MyFormula appear among the MyVar1,MyVar2,. . . ,MyVarn.
9 Structures
A (three-valued) structure with name MyStruct over a vocabulary MyVoc is declared by
structure MyStruct : MyVoc {
// co nt e n ts o f the s t r u c t u r e s
}
or by
f a c t l i s t MyStruct : MyVoc {
// co nt e n ts o f the s t r u c t u r e s
}
9.1 Contents of a structure
A particular input to a problem can be given by giving a (three valued) interpretation to all types
and some predicate and function symbols of a given vocabulary. Here, we describe the different
ways to specify a structure.
15
9.1.1 Type Enumeration
The syntax for a type enumeration is
MyType = { El_1 ; El_2 ; . . . ; El_n }
where MyType is the name of the enumerated type and El_1; El_2; ... ; El_n are the names
of the objects of that type. Names of objects can be (positive and negative) integers, strings, chars,
compound domain elements, or identifiers that start with an upper- or lowercase letter. Identifiers
are shorthands for strings (without the quotes) and can be interchanged within IDP specifications.
In lua-blocks, however, only the string variant should be used.
If one type is a subtype of another, all elements of the subtype are added to the supertype also.
In the case all subtypes of a given type are specified, the supertype is derived to be the union of all
elements of the subtypes. If a type is not specified, all domain elements of that type that occur in
a predicate or function interpretation (see below) are automatically added to that type.
9.1.2 Predicate Enumeration
The syntax for enumerating all tuples for which a predicate MyPred with narguments is true is as
follows.
MyPred = { El_1_1 , . . . , El_1_n ;
. . . ;
El_m_1 , . . . , El_m_n
}
It is also possible to write parentheses around tuples.
MyPred = { ( El_1_1 , . . . , El_1_n ) ;
. . . ;
(El_m_1 , . . . , El_m_n)
}
This notation makes it possible to state that a proposition (a predicate with no arguments) is true,
by using an empty tuple.
t r u e = { ( ) }
f a l s e = { }
However, we recommend using true and false instead of { () } and {}.
9.1.3 Function Enumeration
The syntax for enumerating a function MyFunc with narguments is
MyFunc = { El_1_1 , . . . , El_1_n −> El_1 ;
...;
El_m_1 , . . . , El_m_n −> El_m
}
To give the interpretation of a constant, one can simply write ‘MyConst = El’ instead of ‘MyConst
={->El}’.
16
9.1.4 Three-Valued Predicate/Function interpretations
Three-valued interpretations are given by either
•enumerating the certainly true and certainly false tuples;
•enumerating the certainly true and the unknown tuples;
•enumerating the unknown and the certainly false tuples.
The third set of tuples can than be derived from the two that were given. To specify which tuples
are enumerated, use <ct>,<cf> and <u>. For example
P<ct> = { /∗enumer ation o f the c e r t a i n l y t ru e t u p l e s o f P ∗/}
P<u> = { /∗e num er at ion o f th e unknown t u p l e s o f P ∗/}
9.1.5 Interpretation by Procedures
The syntax
P = procedure MyProc
is used to interpret a predicate or function symbol Pby a procedure MyProc (see below). If Pis an
n-ary predicate, then MyProc should be an n-ary procedure that returns a boolean. If Pis an n-ary
function, then MyProc should be and n-ary function that returns a number, string, or compound
domain element (depending on the return type of P).
9.1.6 Shorthands
Shorthands like ‘MyType = {1..10; 15..20}’ or ‘MyType = { a..e; A..E }’ may be used for
enumerating types or predicates with only one argument.
9.2 factlist
A factlist consists of a list of facts in the usual syntax symbolname(list of domain elements)..
Semantically, a factlist is the structure which:
•All facts are true in the structure.
•All other atoms are false.
Currently, three-valued structures, structures which are partially given and partially defined (as in
standard ASP for example) and function interpretations cannot be specified in factlists.
10 Procedures
10.1 Declaring a procedure
A procedure with name MyProc and arguments A1, . . . , An is declared by
17
procedure MyProc (A1 , . . . , An) {
// c o n t e n t s o f t h e p r o ce d ur e
}
Inside a procedure, any chunk of Lua code can be written. For Lua’s reference manual, see http:
//www.lua.org/manual/5.1/. In the following, we assume that the reader is familiar with the
basic concepts of Lua. Like in most programming languages, a procedure should be declared before
it can be used in other procedures (either in the same file or in earlier included files). There is one
exception to this: procedures in the global namespace (for example, all built-in procedures) can
always be used, no matter what.
10.2 IDP types
Besides the standard types of variables available in Lua, the following extra types are available in
IDP procedures.
sort A set of sorts with the same name. Can be used as a single sort if the set is a singleton.
predicate_symbol A set of predicates with the same name, but possibly with different arities.
Can be used as a single predicate if the set is a singleton. If Pis a predicate_symbol and
nan integer, then P/n returns a predicate_symbol containing all predicates in Pwith arity
n. If s1, . . . , sn are sorts, then P[s1,...,sn] returns a predicate_symbol containing all
predicates Q/n in P, such that the i’th sort of Qbelongs to the set si, for 1≤i≤n.
function_symbol A set of first-order functions with the same name, but possibly with different
arities. Can be used as a single first-order function if the set is a singleton. If Fis a func-
tion_symbol and nan integer, then F/n:1 returns a function_symbol containing all function
in Fwith arity n. If s1, . . . , sn,tare sorts, then F[s1,...,sn:t] returns a function_symbol
containing all functions G/n in F, such that the i’th sort of Fbelongs to the set si, for
1≤i≤n, and the output sort of Gbelongs to t.
symbol A set of symbols of a vocabulary with the same name. Can be used as if it were a sort,
predicate_symbol, or function_symbol.
vocabulary A vocabulary. If Vis a vocabulary and sa string, V[s] returns the symbols in Vwith
name s.
compound A domainelement of the form F(d1, . . . , dn), where Fis a first-order function and d1,
. . . , dnare domain elements.
tuple A tuple of domain elements. T[n] returns the n’th element in tuple T(This is 1-based, thus
the first element is referred to as T[1]).
predicate_table A table of tuples of domain elements.
predicate_interpretation An interpretation for a predicate. If Tis a predicate_interpretation,
then T.ct,T.pt,T.cf,T.pf return a predicate_table containing, respectively, the certainly
true, possibly true, certainly false, and possibly false tuples in T.
18
function_interpretation An interpretation for a function. F.graph returns the predicate_interpretation
of the graph associated to the function_interpretation F.
structure A first-order structure. To obtain the interpretation of a sort, singleton predicate_symbol,
or singleton function_symbol symb in structure S, write S[symb].
theory A logic theory.
options A set of options.
namespace A namespace.
overloaded An overloaded object.
10.3 Built-in procedures
A lot of procedures are already built-in. The command help() gives you an overview of all available
sub-namespaces, procedures,. . . . The stdspace namespace contains all built-in procedures.
10.3.1 stdspace
The stdspace contains the following procedures:
elements(d) Returns a procedure, stopargument, and a beginindex (hence, a Lua-iterator) such
that “for e in elements(d) do ... end” iterates over all elements in the given domain d.
help(namespace) List the procedures in the given namespace.
idptype(something) Returns custom typeids for first-class idp citizens.
tuples(table) Returns a Lua-iterator such that “for t in tuples(table) do ... end” iterates over all
tuples in the given predicate table.
All procedures in stdspace are included in the global namespace and hence can be called by
procedure() instead of by stdspace.procedure().
Furthermore: stdspace contains the following subnamespaces:
idpintern
inferences
options
structure
theory
vocabulary
10.3.2 idpintern
This namespace contains procedures that are either only for internal use or still under development
/ testing. Using them is at your own risk. idpintern is not included in the global namespace; help
for idpintern can be obtained by help(stdspace.idpintern).
19
10.3.3 inferences
The inferences namespace and all its procedures are included in the global namespace. Hence
inferences.xxx should never be used. This namespace contains several inference methods:
allmodels(theory,structure) Returns all models of the theory that extend the given structure.
calculatedefinitions(theory,structure) Make the structure more precise than the given one by
evaluating all definitions with known open symbols. This procedure works recursively: as
long as some definition of which all open symbols are known exists, it calculates the definition
(possibly deriving open symbols of other definitions). This procedure returns a new structure
or nil if inconsistency is detected.
explainunsat(theory, structure, vocabulary) Given input structure Si, input theory Tiand
vocabulary Vi, this procedure searches for a structure SOand a theory TOsuch that the
following hold * SOis less precise than Si.
TOis entailed by Ti(obtained by instantiating universal quantifiers in rules and sentences)
SOequals Sion symbols not in Vi
SOis maximally imprecise with respect to the above criteria
TOis maximally restrictive w r t the above criteria
Furthermore, this procedure also prints SOand TOin a human-readable way (note: with
respect to definitions, the entailment is not always strictly respected since it is currently
impossible to partially define symbols)
ground(theory,structure) Create the reduced grounding of the given theory and structure.
groundeq(theory,structure,modeleq) Create the reduced grounding of the given theory and
structure. modeleq is a boolean parameter: whether or not the grounding should preserve
the number of models (it always preserves satisfiability but might not preserve the number of
models if modeleq is false).
printgrounding(theory,structure) Print the reduced grounding of the given theory and struc-
ture. MEMORY EFFICIENT: does not store the grounding internally.
groundpropagate(theory,structure) Return a structure, made more precise than the input by
grounding and unit propagation on the theory. Returns nil when propagation makes the
givens structure inconsistent.
optimalpropagate(theory,structure) Return a structure, made more precise than the input
by generating all models and checking which literals always have the same truth value This
propagation is complete: everything that can be derived from the theory will be derived.
Returns nil when propagation results in an inconsistent structure.
propagate(theory,structure) Returns a structure, made more precise than the input by doing
symbolic propagation on the theory. Returns nil when propagation results in an inconsistent
structure.
20
initialise(theory,structure) can only be called with an LTC theory. Performs initialisation for
the progression inference1. It returns a table consisting of a number (depending on stdop-
tions.nbmodels) of models, and the used bistate theory, the initial theory, the bistate vocab-
ulary and the initial vocabulary.
progress(theory,structure) can only be called with an LTC theory. Performs one progression
step for the progression inference1
isinvariant(theory, theory) uses a theorem prover (set by stdoptions.provercommand) to try to
prove that the second theory is an invariant of the first theory. The second theory should be
of the form : ∀t[T ime] : ϕ[t], where ϕcan be a single-state formula or a bistate formula and
the first should be an LTC theory. It uses the methods presented in progression inference1.
isinvariant(theory, theory, structure) uses the model expander to prove that the second theory
is an invariant of the first theory in the context of the given structure. The second theory
should be of the form : ∀t[T ime] : ϕ[t], where ϕcan be a single-state formula or a bistate
formula and the first should be an LTC theory. It uses the methods presented in progression
inference1.
minimize(theory,structure,term,vocabulary) The structure can interpret a subvocabulary of
the vocabulary of the theory, the vocabulary of the theory and the term have to be identical.
The fourth argument (vocabulary) is optional and allows you to specify a subvocabulary
containing only the symbols in which you’re interested. It returns (1) a table of all models
of the theory that extend the given structure and such that the term is minimal, (2) a
boolean indicating whether an optimum was found, (3) the optimal value of the term, and, if
stdoptions.trace == true, (4) a trace of the solver.
modelIterator(theory, structure, vocabulary) Returns an iterator iterating over all possible
two-valued models satisfying the given theory. See modelexpand for more information.
i t e r a t o r = m o d e l I t e r a t o r (T, S ) ;
p r i n t ( " 1 : " , i t e r a t o r ( ) ) ;
p r i n t ( " 2 : " , i t e r a t o r ( ) ) ;
for model i n i t e r a t o r do // p r i n t a l l o t he r models
p r i n t ( model ) ;
end
modelexpandpartial(theory,structure, vocabulary) Apply model expansion to theory T, struc-
ture S. The structure can interpret a subvocabulary of the vocabulary of the theory. The result
is a table of (possibly three-valued) structures that are more precise then S and that satisfy
T and, if stdoptions.trace == true, a trace of the solver. The third argument (vocabulary)
is optional and allows you to specify a subvocabulary containing only the symbols in which
you’re intersted.
modelexpand(theory,structure,vocabulary) Apply model expansion to theory T, structure
S. The structure can interpret a subvocabulary of the vocabulary of the theory. The result
is a table of two-valued structures that are more precise then S and that satisfy T and, if
1See “Simulating Dynamic Systems Using Linear Time Calculus Theories” (Bogaerts et al., 2014)
21
stdoptions.trace == true, a trace of the solver. (this procedure is equivalent to first calling
modelexpandpartial and subsequently calling alltwovaluedextensions) The third argument
(vocabulary) is optional and allows you to specify a subvocabulary containing only the symbols
in which you’re intersted.
onemodel(theory,structure) Does model expansion but only searches for one model (no matter
what the nbmodels option is set to). Returns this structure (in contrast to the standard
modelexpansion which returns a list of structures).
printunsatcore(theory,structure) Finds a theory that is a minimal “subset” of the given theory
that is unsat in the given structure, or, in other words, a “core”; it then prints this theory
with references to how it was obtained from the given theory. A subset in this respect is a
subset of all instantiated formulas in conjunctive context in the theory and instantiated rules
(either all rules defining a specific domain atom/term or none of them). Currently does not
take constraints implied by the vocabulary (e.g., function constraints) or the structure (e.g.,
type interpretations) into account.
printmodels(list) Prints a given list of models or prints unsatisfiable if the list is empty.
query(query,structure) Generate all solutions to the given query in the given structure. The
result is the set of element-tuples that certainly satisfy the query in the structure.
refinedefinitions(theory,structure) Make the structure more precise than the given one by
refining all defined symbols using the definitions until fixpoint. This procedure returns a new
structure or nil if inconsistency is detected.
sat(theory,structure) Checks satisfiability of the given theory-structure combination. Returns
true if and only if there exists a model extending the structure and satisfying the theory.
unsatstructure(theory,structure,vocabulary) Returns a structure S that is less precise than
the input structure such that the given theory has no models that expand S. Furthermore S is
a precision-minimal structure with this property. If the optional third argument is provided,
the resulting structure S must furthermore equal the input structures on all symbols not in
the provided vocabulary.
value(formula/term,structure) Evaluate a variable-free formula or term in a two-valued struc-
ture, returning true/false for a formula and a domainelement or nil for a term.
equal(obj,obj) Compares the contents of two domain elements or tables of domain elements to
see whether they are the same.
10.3.4 options
Like the inferences namespace, the options namespace and all its procedures are included in the
global namespace. This namespace consists of the following procedures:
getoptions() Get the current options.
newoptions() Create new options, equal to the standard options.
setascurrentoptions(options) Sets the given options as the current options, used by all other
commands.
22
10.3.5 structure
Also this namespace and all its procedures are included in the global namespace. Here, you can
find several procedures for manipulating logical structures.
alltwovaluedextensions(structure) This procedures takes one (three-valued) structure and re-
turns all structures over the same vocabulary that extend the given structure and are two-
valued.
alltwovaluedextensions(table) This procedures takes a table of structures and returns all two-
valued extensions of any of the given structures.
clean(structure) Modifies the given structure (the structure is the same, but its representation
changes): transforms fully specified three-valued relations into two-valued ones. For example
if Phas domain [1..2] and in the given structure, P<ct> = {1}, P<cf> = {2}, in the end,
Pis {1}.
clone(structure) Returns a structure identical to the given one.
isconsistent(structure) Check whether the structure is consistent.
makefalse(predicate_interpretation,table) Sets all tuples of the given table to false, indepen-
dent of the previous values (so this will never make the table inconsistent). Modifies the
table-interpretation.
makefalse(predicate_interpretation,tuple) Sets the interpretation of the given tuple to false,
independent of the previous value (so this will never make the table inconsistent). Modifies
the table-interpretation.
maketrue(predicate_interpretation,table) Sets all tuples of the given table to true, indepen-
dent of the previous values (so this will never make the table inconsistent). Modifies the
table-interpretation.
maketrue(predicate_interpretation,tuple) Sets the interpretation of the given tuple to true,
independent of the previous value (so this will never make the table inconsistent). Modifies
the table-interpretation.
makeunknown(predicate_interpretation,table) Sets all tuples of the given table to unknown,
independent of the previous values (so this will never make the table inconsistent). Modifies
the table-interpretation.
makeunknown(predicate_interpretation,tuple) Sets the interpretation of the given tuple to
unknown, independent of the previous value (so this will never make the table inconsistent).
Modifies the table-interpretation.
merge(structure,structure) Create a new structure which is the result of combining both input
structures. The union of the elements in the sorts are taken. For predicates/functions, the
union of the certainly falses and certainly trues are taken. This means that the resulting
structure can be inconsistent (if an element was present in the cf of one structure and the
ct of another) or can become three-valued, even if the two original ones are two-valued (if a
sort is extended through one argument, and the predicates interpreting that sort in the other
argument, are not extended.
23
newstructure(vocabulary,string) Create an empty structure with the given name over the given
vocabulary.
createdummytuple() Create an empty tuple.
iterator(domain) Create an iterator for the given sorttable.
iterator(predicate_table) Create an iterator for the given predtable.
size(predicate_table) Get the size of the given table.
range(number,number) Create a domain containing all integers between First and Last.
10.3.6 theory
The theory namespace and all its procedures are included in the global namespace. It contains
methods for manipulating theories, most of which modify the given theory.
clone(theory) Returns a theory identical to the given one.
completion(theory) Add definitional completion of all the definitions in the theory to the given
theory. Modifies its argument.
flatten(theory) Rewrites formulas with the same operations in their child formulas by reducing
the nesting. For example a∧(b∧c)will be rewritten to a∧b∧c. Modifies the given theory.
merge(theory,theory) Create a new theory which is the result of combining (the conjunction of)
both input theories.
pushnegations(theory) Push negations inwards until they are right in front of literals. Modifies
the given theory.
removecardinalities(theory,int) Replaces atoms consisting of a cardinality term compared with
an integer term, if the latter is smaller or equal to the given integer (or if that is zero), with
an equivalent FO formula. Modifies the given theory.
removenesting(theory) Move nested terms out of predicates (except for the equality-predicate)
and functions. Modifies the given theory.
10.3.7 vocabulary
The vocabulary namespace and all its procedures are included in the global namespace. It contains
methods for setting and getting vocabularies.
getvocabulary(query) Returns the vocabulary of the given object.
getvocabulary(structure) Returns the vocabulary of the given object.
getvocabulary(term) Returns the vocabulary of the given object.
getvocabulary(theory) Returns the vocabulary of the given object.
setvocabulary(structure,vocabulary) Changes the vocabulary of a structure to the given one.
newvocabulary(string) Create an empty vocabulary with the given name.
24
10.3.8 Miscellaneous
parse(string) Parses the given file and adds its information into the datastructures.
10.3.9 The table_utils library
The table_utils standard library file can be include by
include <t a b l e _ u t i l s >
It contains several useful commands for manipulating tables, converting predicate tables to lua-
tables.
printtuples(name, table) Given a predicate name and a relationship table, prints all tuples in
the table
tablecontains(table, element) Returns true if a given table contains a certain element
totable(input) Converts the input to a lua-table. The input can be a domain, predicate table or
a tuple.
11 Options
The IDP system has various options. To print the current values of all options, use print(getoptions()).
To set an option, you can use the following lua-code
s t d o p t i o n s . MyOption = MyValue
where MyOption is the name of the option and MyValue is the value you want to give it. If you
want to have multiple option sets, you can make them with them with
F i r s t O p t i o n S e t = newO ption s ( )
SecondO pt io nSet = newOptions ( )
F i r s t O p t i o n S e t . MyOption = MyValue
SecondOptionSet . MyOption = MyValue
To activate an option set, use the procedure setascurrentoptions(MyOptionSet). From that
moment, MyOptionSet will be used in all comands.
11.1 Verbosity options
grounding = [0..max(int)] Verbosity of the grounder. The higher the verbosity, the more debug
information is printed.
solving = [0..max(int)] Like groundverbosity, but controls the verbosity of MiniSAT(ID)
propagation = [0..max(int)] Like grounding, but controls the verbosity of the propagation.
symmetrybreaking = [0..max(int)] Like grounding, but controls the verbosity of the symmetry
detection and breaking routine.
25
approxdef = [0..5] Verbosity of the module that uses an approximating definition to perform
approximation prior to grounding and solving.
functiondetection = [0..max(int)] Verbosity of the module that detects functions and rewrites
a theory accordingly.
calculatedefinitions = [0..5] Verbosity of the module that calculates definitions prior to ground-
ing and solving.
•1 or greater: print when calculating the definition starts and ends. Also prints the input-
and outputstructure of the process.
•2 or greater: print for each definition separately when it is being calculated and print
when it is being calculated using XSB.
•3 or greater: print XSB code that will be used to calculate the definitions.
•5 or greater: print queries that are being sent to XSB and the answer tuples they return.
11.2 Modelexpansion options
nbmodels = [0..max(int)] Set the number of models wanted from the modelexpansion inference.
If set to 0, all models are returned.
trace = [false, true] If true, the procedure modelexpand produces also an execution trace of
MiniSAT(ID).
cpsupport = [false, true] If true, constants can occur in the grounding, which are taken care of
through integration with Constraint Programming techniques.
cpgroundatoms = [false, true] If true, the grounding can be full ground FO(.), which has an
even smaller grounding (but might have reduced propagation).
functiondetection = [false, true] If true, function detection is used to replace predicate symbols
by function symbols with smaller arity.
skolemize = [false, true] If true, existential quantification in sentences is replaced by introducing
new function symbols. Only advantageous with cpsupport on.
tseitindelay = [false, true] If true, grounding can be delayed by lazily expanding quantifications
and disjunctions/conjunctions.
satdelay = [false,true] If true, grounding can be delayed by maintaining justifications for non-
ground sentences and rules.
symmetrybreaking = [none,static] If the symmetry breaking option "static" is chosen, an au-
tomatic symmetry detection routine detects sets of interchangeable domain elements. These
induce symmetry groups on the set of models to the modelexpansion problem, which are bro-
ken using static symmetry breaking constraints. Activating this option may invalidate some
models, but if the problem is satisfiable, at least one model satisfies the symmetry breaking
constraints.
26
11.3 Propagation options
groundwithbounds = [false, true] Enable/disable bounded grounding (if enabled, first do sym-
bolic propagation to provide ct and cf bounds for formulas to reduce the size of the grounding
in every inferences that grounds (groundpropagate/ground/modelexpand/...)).
longestbranch = [0..2147483647] The longest branch allowed in BDDs during propagation.
The higher, the more precise the propagation will be (but also, the more time it will take).
nrpropsteps = [0..2147483647] The number of propagation steps used in the propagate-inference.
The higher, the more precise the propagation will be (but also, the more time it will take).
relativepropsteps = [false, true] If true, the total number of propagation steps is nrpropsteps
multiplied by the number of formulas.
11.4 Printing options
language = [ecnf, idp, idp2 tptp] The language used when printing objects. Note, not all lan-
guages support all kinds of objects.
longnames = [false, true] If true, everything is printed with reference to their vocabulary. For
example, a predicate Pfrom vocabulary Vwill be printed as V::P instead of P.
11.5 Entailment options
provercommand = string String is the command by which a theorem prover can be called (as
on a command-line). It has to contain the placeholders %i and %o which will be replaced with
the input and output file, respectively.
proversupportsTFA = [false, true] Should be set to true if the selected prover (using above
command) supports to TFA syntax of the CASC competition (Typed Fo with Arithmetic).
Otherwise FOF syntax (First-Order Formulas) will be used.
11.6 General options
assumeconsistentinput = [false, true] If true, input structures are not checked for consistency
(which can be expensive to verify).
xsb = [false, true] Enable/disable the usage of XSB.
timeout = [0..max(int)] Set the time after which an inference is requested to stop gracefully
(in seconds, 0 indicates no timeout). In interactive mode, this is one lua call, otherwise the
execution of the command supplied by “-e” (or the main procedure) is timed. Whenever a
timeout is reached, the inference is provided with 10 seconds to exit gracefully, otherwise the
system aborts.
memoryout = [0..max(int)] Similar to the above, but monitors the memory usage (in Mb).
27
mxtimeout = [0..max(int)] Similar to above, but only times calls to model expansion and mini-
mization. If any models have already been found, they are returned properly. In case of model
optimization, the best model(s) found to date are returned, not guaranteeing optimality has
been proven.
mxmemoryout = [0..max(int)] Similar to the above, but monitors the memory usage (in Mb).
seed = [0..max(int)] Set the seed for the random generator (used in the estimators for BDDs
and in the SAT-solver).
approxdef = ["none", "complete", "cheap"] none : do not use any approximating definition
complete : use the complete approximating definition
cheap : use the approximating definition without certain expensive rules
randomvaluechoice = [false, true] Controls the solver: if set to true, the assignment to choice
literals is random, if set to false, the solver default assigns false to choice literals.
12 IDP2vs IDP3
Users of the old IDP2-system will still have a bunch of files with different syntaxis. Here are the
basic rules for transforming them to IDP3.
•Blocks in the IDP2system now are structures, vocabularies and theories.
–Everything that used to be in a Given: Declare: or Find: block, now belongs to a
vocabulary.
–The sentences and definitions from the Satisfying: block should be moved to a theory.
–The Data: block is essentialy what is now a structure.
•UNA-DCA declarations in the vocabulary are no longer allowed:
–In the IDP2system you could write type Direction=Up;Down. This had the effect of
creating new domain elements Up and Down and constants Up and Down that could be
used in the theory (Satisfying block).
–For the moment, this is not yet possible in the IDP3system. If you want the same effect:
you add type Direction,Up: Direction and Down: Direction to the vocabulary
(this creates the type and makes the constants. In the structure, you interprete Direction
by Direction = u;d and you interprete the constants by Up = u; Down = d.
•Three-valued interpretations have a slightly different syntax.
–In a Data: block of the IDP2system, one could write P = A;BC, meaning that Pshould
be certainly true for Aand Band that Pshould be certainly false for C. In IDP3, we
write (as explained above P<ct> = A;B and P<cf> = C.
•Aggregates have a slightly different syntaxis (see above).
28
13 Common errors and warnings
In this section the most common error and warning messages you might encounter are listed and a
short explanation is given. Some general recommendations:
•Earliest exception first: As one error might propagate to more errors in code which is in fact
correct, always start resolving errors from the first one encountered.
•Warnings are important: Usually, warnings notify that some part of the specification can
be interpreted in multiple ways (and the system tells you which choice it made) or that the
system suspects you made an error, although the specification does not violate any rule. So
always at least verify whether the correct resolution was made and preferably change the
specification to remove the warning.
13.1 Syntax error
“” Some part of the specification is invalid FO(·)IDP syntax. Some possible fixes might be presented
by the system. General recommendations to prevent this kind of errors:
•Declare all symbols in the vocabulary and check the number of arguments.
•Check the number of brackets.
•Variables are separated by whitespace, arguments by commas and tuples by “;”.
13.2 Unquantified variables
“” The system encountered a 0-ary symbol which was not quantified and not declared in the
vocabulary. It assumes it is then a variable which is taken to have the default quantification in the
context in which it occurs, but warns you as you might have intended another quantification or had
intended it to be some other or undeclared predicate or constant symbol.
13.3 Derived type
“” This warning is produced if the type of a variable or term is ambiguous. It makes a usually safe
guess to the intended type, but it should at least be checked and preferably stated explicitly.
13.4 Underivable type
“” In some cases, there are multiple types possible and no safe guess is available, such as two possible
types which have no related parents. In that case, the intended type has to be stated explicitly.
13.5 Infinite grounding
“” When constructing the grounding, the system might detect that it has to make an infinite
grounding (it can also go undetected in some cases). It is guaranteed that this will not happen
using default options if all variable types are explicitly stated and no infinite types are used for any
variable or argument type (parent types can be infinite).
29
