First-Order Logics in Tarski

A number of classical planning representation languages such as STRIPS or Functional STRIPS have their roots in the logical tradition and use, to different degrees, first-order language concepts in order to succinctly encode the dynamics of the planning problem to be represented. Tarski also builds on these ideas, making as clear as possible a distinction between the first-order language used to define a problem and the actual problem itself. In this tutorial, we’ll have a look at the logical capabilities of Tarski.

Theories and many-sorted languages

Due to its closeness to the standard planning modeling languages, Tarski uses many-sorted logics, a refinement of first-order logics in which variables can have different sorts (also: types), and hence range over different domains, or disjoint subsets of the universe of discourse.

Additionally, Tarski borrows from the SMT literature the idea of using predefined theories, each of which incorporates into the language a number of standard sorts and predicate and function symbols.

Let us start by creating a first-order language with the predefined equality and arithmetic theories:

import tarski
lang = tarski.language(name='tutorial', theories=['equality', 'arithmetic'])
lang

tutorial: Tarski language with 4 sorts, 6 predicates, 9 functions and 0 constants

lang is now a first-order language with sorts such as the default object sort, but also the integer, real and natural sorts. Thanks to the built-in theories, it also incorporates standard arithmetic predicates such as \(=\), \(\neq\), \(\leq\), etc.

lang.sorts

[Sort(object), Sort(Real), Sort(Integer), Sort(Natural)]

lang.predicates

[=/2, !=/2, </2, <=/2, >/2, >=/2]

lang.functions

[ite/2, @/2, +/2, -/2, */2, //2, **/2, %/2, sqrt/1]

Let us define a couple of non-builtin sorts block and place for a hypothetical Blocks world:

block = lang.sort('block')
place = lang.sort('place')

Declaring domain constants

Due again to its closeness to the standard practice in planning and related disciplines such as logic programming, Tarski partially adopts the Herbrand-like convention that all constant symbols denote themselves. It is for this reason that there is a separate mechanism to declare language constants (which in action languages such as PDDL are often also called “objects”):

b1 = lang.constant('b1', block)
b2 = lang.constant('b2', block)
table = lang.constant('table', place)

Each of the above calls declares constants of given types (block or place), which are enforced to denote themselves - i.e., any interpretation for this language will feature an element \(table\) in the domain of sort \(place\), and elements \(b1\) and \(b2\) in the domain of sort \(block\).

Tarski allows to declare constants both using sort objects (such as \(place\)), or simply their name (e.g., “place”). Of course we can also use standard Python idioms such as list comprehensions to save some typing. Say we want to declare 20 more blocks:

forty = [lang.constant(f"b{k}", "block") for k in range(3, 21)]

At any point we can inspect all constants declared so far:

lang.constants()

[b1 (block),
 b2 (block),
 table (place),
 b3 (block),
 b4 (block),
 b5 (block),
 b6 (block),
 b7 (block),
 b8 (block),
 b9 (block),
 b10 (block),
 b11 (block),
 b12 (block),
 b13 (block),
 b14 (block),
 b15 (block),
 b16 (block),
 b17 (block),
 b18 (block),
 b19 (block),
 b20 (block)]

as well as retrieve any of the sorts declared so far:

lang.get_sort('place')

Sort(place)

Sort hierarchies

Tarski implements a rudimentary sort hierarchy mechanism…

TO-DO! :-)

Built-in sorts

Tarski languages can optionally contain some built-in sorts to help the modeller e.g. use common algebraic predicates without having to define everything from first principles. At the time of writing, every Tarski language comes with the following built-in sorts

• object - the base, default sort.

• Real - the set of real numbers \(\mathbb{R}\)

• Integer - the set of integer numbers \(\mathbb{Z}\)

• Natural - the set of natural numbers \(\mathbb{N}\)

Sort object is always defined, whereas the other three are only defined if the language is created with the arithmetic theory. The three arithmetic sorts are represented as closed intervals with well-defined lower and upper bounds. We cannot introduce symbols into built-in sorts, but we can refer to them with Python variables:

lang.constant(3, lang.Real)

3.0 (Real)

lang.constant(42, lang.Integer)

42 (Integer)

or even

import numpy as np
lang.constant(np.pi, lang.Real)

---------------------------------------------------------------------------
ModuleNotFoundError                       Traceback (most recent call last)
/tmp/ipykernel_391/3602549491.py in <module>
----> 1 import numpy as np
      2 lang.constant(np.pi, lang.Real)

ModuleNotFoundError: No module named 'numpy'

Built-in sorts can be accessed either with the standard get_sort() accessor, or directly on the language:

assert lang.get_sort('Real') == lang.Real

And can be easily distinguished because of their attribute builtin:

lang.Real.builtin

True

Intervals

So far the kind of sorts we have seen are either sets defined arbitrarily, or an infinite subset of the \({\mathbb R}\) continuum (e.g. Real is actually a subset of the rationals \({\mathbb{Q}}\)). One special case of sort is that which is a subset of the Cartesian product of its domain with itself, which we refer to as intervals. These subsets are assumed to be dense, and allow to represent without loss of generality sorts like

\[I \equiv [a,b],\ \text{where}\, a,b \in {\mathbb Z}\]

or some other built-in sort.

We can declare the interval sort for \([0,10]\) where \(0\) and \(10\) are taken to be integers as follows

I = lang.interval('I', lang.Integer, 0, 10)

Constants are then given as in the unrestricted case

one = lang.constant(1, I)

Trying to creat constants of interval types which aren’t consistent with the declared bounds will result in an exception

try:
    lang.constant(-2, I)
except ValueError as err:
    print("Caught exception: {}".format(err))

Caught exception: Cast: Symbol '-2' (encoded '-2') outside of defined interval bounds

A Hierarchy of Sorts

Sorts associated to a language can be arranged as per hierarchy, specifying the partial ordering relation \(\sqsubseteq\) to hold between two given sorts \(\alpha\) and \(\beta\)

alpha = lang.sort('alpha')

beta = lang.sort('beta', alpha)

The parent of \(\beta\), that is, the sort \(\alpha\) s.t. \(\alpha \sqsubseteq \beta\), is accessible via the method parent

print("Parent of {} is {}".format(beta, tarski.syntax.sorts.parent(beta)))

Parent of Sort(beta) is Sort(alpha)

For built-in sorts, this relationship is already defined as expected

R = lang.Real

print("Parent of {} is {}".format(R, tarski.syntax.sorts.parent(R)))

Parent of Sort(Real) is Sort(object)

Z = lang.Integer

print("Parent of {} is {}".format(Z, tarski.syntax.sorts.parent(Z)))

Parent of Sort(Integer) is Sort(Real)

N = lang.Natural

print("Parent of {} is {}".format(N, tarski.syntax.sorts.parent(N)))

Parent of Sort(Natural) is Sort(Integer)

Constants, Functions and Predicates

Let’s start populating the language bw for describing instances of Blocks World

import tarski
import tarski.errors as err

bw = tarski.language()

Blocks Worlds are made of objects of two sorts:

place = bw.sort('place')

and

block = bw.sort('block', place)

We populate our instance with a few blocks

b1, b2, b3, b4 = [ bw.constant('b_{}'.format(k), block )  for k in (1,2,3,4) ]

and a table

table = bw.constant('table', place)

Functions

Function symbols \(f\) are used to represent mappings between several sorts \(\tau\). Formally, we will define \(f\) as mappings

\[f : \tau_1, \ldots, \tau_n \mapsto \tau_{n+1}\]

Functions \(f\) have arity \(n \geq 0\), their domain is the cartesian product \(\tau_1 \times \tau_2 \ldots \times \tau_n\) and their codomain is the sort \(\tau_{n+1}\). The signature \(\sigma_f\) of \(f\) corresponds with the tuple

\[(f, \tau_1, \ldots, \tau_n, \tau_{n+1})\]

and allows to uniquely identify a function: Tarski doesn’t allow languages with functions \(f\) and \(f'\) such that \(\sigma_f\) \(=\) \(\sigma_{f'}\).

For Blocks World we can define the function \(loc: block \mapsto place\), which we use to refer indirectly to the object a given block is on top of at any point in time

loc = bw.function('loc', block, place)

We note that the arguments of this method correspond with the components of a function signature, hence

print('Domain of {}: {}'.format(loc, loc.domain))
print('Codomain of {}: {}'.format(loc, loc.codomain))
print('Type of {}: {}'.format(loc, loc.sort))
print('Arity of {} : {}'.format(loc, loc.arity))

Domain of loc/1: (Sort(block),)
Codomain of loc/1: Sort(place)
Type of loc/1: (Sort(block), Sort(place))
Arity of loc/1 : 1

Printing function objects indicates the arity (number of arguments) the function was declared with, following the convention typically used in Prolog.

Predicates as Relation Symbols

Relations between objects and intrinsic properties of objects are modelled by means of relation symbols or predicates.

clear = bw.predicate('clear', block )

By default, Tarski languages do not define implictly any kind of builtin predicate or function. For instance, if we try to write something like

try:
    b1 == b2
except err.LanguageError as e:
    print(f"Caught exception {e}")

Caught exception Operator '=' not defined on domain (<class 'tarski.syntax.terms.Term'>, <class 'tarski.syntax.terms.Term'>)

For that we need to explicitly attach theories to our language, as shown later.

Terms and Formulas

Now we have all the elements to formally define Tarski languages:

Definition (Many-Sorted First-Order Language). A many-sorted first-order language \({\cal L}\) is made up of: - A non-empty set \(T\) of sorts - An infinite number of variables \(x_{1}^{\tau}, x_{2}^{\tau}, \ldots\) for each short \(\tau \in T\) - For each \(n \geq 0\) and each tuple \((\tau_1, \ldots, \tau_{n+1}) \in T^{n+1}\) of sorts, a (possibly empty) set of function symbols, each of which is said to have arity and type \((\tau_1, \ldots, \tau_{n+1})\) - For each \(n \geq 0\) and each tuple \((\tau_1, \ldots, \tau_{n+1}) \in T^{n}\) of sorts, a (possibly empty) set of relation symbols (predicates), each of which is said to have arity and type \((\tau_1, \ldots, \tau_{n})\)

Continuing with our Blocks World themed example

import tarski
from tarski.syntax import *
from tarski.theories import Theory

# 1. Create language used to describe world states and transitions
bw = tarski.language(theories=[Theory.EQUALITY, Theory.ARITHMETIC])

# 2. Define sorts
place = bw.sort('place')
block = bw.sort('block', place)

# 3. Define functions
loc = bw.function( 'loc', block, place )
looking_at = bw.function( 'looking_at', block )

# 4. Define predicates
clear = bw.predicate( 'clear', block)

We introduce the function \(width(b)\) for blocks \(b\), this will allow us to specify Hanoi Towers like tasks

width = bw.function('width', block, bw.Real)

Constants are 0-arity functions, whose sort \(\tau\) is a set with one single element. Hence, we handle them separately, as we specialise their representation

# 5. Define constants
b1, b2, b3, b4 = [ bw.constant('b_{}'.format(k), block) for k in (1,2,3,4) ]
table = bw.constant('table', place)

(First-Order) Terms

Combinations of variables, functions and constants are called terms, and the rules for constructing them are given inductively:

Definition (First-Order Terms). A term \(t\) can be:

• Any variable \(x^{\tau}\) of the language can be a term \(t\) with type \(\tau\)

• Any constant symbol of the language with type \(\tau\) is a term with the same type

• If \(t_1, \ldots, t_n\) are terms with respective types \(\tau_1, \ldots, \tau_n\) and \(f\) is a function symbol with type \((\tau_1, \ldots, \tau_n, \tau{n+1})\) then \(f(t_1,\ldots,t_n)\) is a term with type \(\tau_{n+1}\).

Terms are implemented as Python objects. Every constant symbol is an instance of Term

from tarski import Term

isinstance(b1,Term)

True

Function symbols allow to nest terms, thus

t1 = loc(b1)
isinstance(t1,Term)

True

x = bw.variable('x', block)
t2 = loc(x)
isinstance(t2,Term)

True

t3 = loc(looking_at())
isinstance(t3,Term)

True

are all terms. Tarski textual representation of variables is a bit different

print('{}, type: {}'.format(t1, t1.sort))
print('{}, type: {}'.format(t2, t2.sort))
print('{}, type: {}'.format(t3, t3.sort))

loc(b_1), type: Sort(place)
loc(x), type: Sort(place)
loc(looking_at()), type: Sort(place)

in order to make distinct variables from constants, the former are printed with the prefix ?.

Formulas

Formulas (statements that can be either True or False) are defined also inductively as follows:

Definition (First-Order Formulas).

• If \(t_1\) and \(t_2\) are two terms with the same type, then \(t_1 = t_2\) is an atomic formula.

• If \(t_1,\ldots,t_n\) are terms with respective types \(\tau_1,\ldots,\tau_n\), and \(R\) is a relation symbol with type \((\tau_1,\ldots,\tau_n)\), then \(R(t_1,\ldots,t_n)\) is an atomic formula too.

• If \(\phi_1\) and \(\phi_2\) are formulas then \(\neg \phi_1\), \(\phi_1 \lor \phi_2\) and \(\phi_1 \land \phi_2\) are also formulas.

• If \(\phi\) is a formula, then \(\exists_t x^{\tau}\, \phi\) and \(\forall_t x^{\tau}\, \phi\) are also formulas.

Quantification happens over a certain sort, i.e. for each sort \(\tau\) \(\in\) \(T\) there are universal and existential quantifier symbols \(\forall_{\tau}\) and \(\exists_{\tau}\), which may be applied to variables of the same sort.

Formulas without existential (\(\exists\)) or universal (\(\forall\)) quantifiers are called quantifier free.

Examples

We can define the formula \(t_1 = t_3\) - terms \(t_1\) and \(t_3\) are equal - with the following statement

tau = t1 == t3

The str() method is overwritten for every term and formula class, returning a string representation of expression, which gives insight into how Tarski represents internally formulas and expressions

str(tau)

'=(loc(b_1),loc(looking_at()))'

We need a new variable so we can make general statements about more than one block

y = bw.variable('y', block)

Now we can state properties of states like for every block x, x cannot be wider than the place below

\[\forall x,y\, loc(x) = y \supset width(x) < width(y)\]

which can be written as

phi = forall( x, y, implies( loc(x) == y, width(x) < width(y) ) )

which is represented internally

str(phi)

'forall x, y : (((not =(loc(x),y)) or <(width(x),width(y))))'

It’s worth noting that Tarski will always try to simplify formulas. For instance, the sub-formula

\[loc(x) = y \supset width(x) < width(y)\]

was transformed into the disjunction

\[loc(x) \neq y \lor width(x) < width(y)\]

using the transformation

\[p \supset q \equiv \neg p \lor q\]

We can use the operator > instead of the function implies(), if a more concise syntax is preferred.

phi = forall( x, y, (loc(x) == y) > (width(x) < width(y)) )

We can write the conjunctive formula

\[loc(b1) \neq loc(b2) \land loc(b1) \neq loc(b3)\]

in several ways. One is using the land function

phi = land( loc(b1) != loc(b2), loc(b1) != loc(b3))

or the operator &

phi = (loc(b1) != loc(b2)) & (loc(b1) != loc(b3))

Another state invariant like

\[loc(b1) = b2 \lor loc(b1) = b3\]

can be written as

phi = lor( loc(b1) == b2, loc(b1) == b3 )

or

phi = (loc(b1)==b2) | (loc(b1)==b3)

Finally, the formula

\[loc(b1) = b2 \supset \neg clear(b2)\]

can be written as

phi=implies( loc(b1) == b2, neg(clear(b2)))
str(phi)

'((not =(loc(b_1),b_2)) or (not clear(b_2)))'

or, alternatively the ~ unary operator can be used instead of neg

phi = implies( loc(b1) == b2, ~clear(b2))
str(phi)

'((not =(loc(b_1),b_2)) or (not clear(b_2)))'

Semantics of First-Order Languages

import tarski

# 1. Create language used to describe world states and transitions
bw = tarski.language(theories=['equality', 'arithmetic'])

# 2. Define sorts
place = bw.sort('place')
block = bw.sort('block', place)

# 3. Define functions
loc = bw.function( 'loc', block, place )
width = bw.function('width', block, bw.Real)

# 4. Define predicates
clear = bw.predicate( 'clear', block)

The semantics of a first-order language is based on the notion of models:

Definition (First-Order logic model). Let \({\cal L}\) be a many-sorted first-order language. A first-order model, sometimes also called structure or interpretation, for the language \({\cal L}\) is a tuple

\[{\cal M} = \langle \{ {\cal U}_{\tau}\},\, \{f^{{\cal M}}\},\, \{P^{{\cal M}}\} \} \rangle\]

made up of:

• A non-empty set \({\cal U}_{\tau}\), the universe of type \(\tau\), for each \(\tau \in T\).

• For each \(n\)-ary function symbol \(f\) of the language with type \((\tau_1, \ldots, \tau_n, \tau_{n+1})\), a function \(f^{\cal M}\) \(:\) \({\cal U}_{\tau_1} \times \ldots \times {\cal U}_{\tau_n} \rightarrow {\cal U}_{\tau_{n+1}}\). When \(n=0\) and \(f\) is a constant symbol of type \(\tau\), \(f^{\cal M}\) is simply some element of the universe \({\cal U}_{\tau}\).

• For each \(n\)-ary predicate symbol \(P\) of type \((\tau_1,\ldots,\tau_n)\), a subset \(P^{\cal M} \subseteq {\cal U}_{\tau_1} \times \ldots \times {\cal U}_{\tau_n}\). If \(n=0\), we will assume that \(P^{\cal M}\) is a truth table \(P^{\cal M}\) \(\in\) \(\{ \top, \bot \}\).

Denotation of Terms and Truth of Formulas

The notion of denotation of a term and truth of a formula under a given interpretation reqyures that we take into account all possible free variables occurring in the term or formula. We will do that by extending interpretations with a type–consistent assignment of values to free variables. Let \(\phi[\bar{x}]\) be a formula in a first-order language \({\cal L}\), and \({\cal M}\) an interpretation for \({\cal L}\). A variable assignment \(\sigma\) for \(\bar{x}\) is a function mapping any free variable \(x^{\tau}\) in the tuple \(\bar{x}\) to an element in \({\cal U_{\tau}}\).

Assignments \(\sigma\) can be easily extended into a function \(\sigma^{*}\) that gives the denotation of any term in the language, being defined as follows:

1. For any variable \(x\), \(\sigma^*(x) = \sigma(x)\)

2. For terms \(t_1\), \(\ldots\), \(t_n\) and \(n\)-ary function symbol \(f\) with matching type

   \[\sigma^*(f(t_1,\ldots,t_n)) = f^{\cal M}(\sigma^*(t_1),\ldots,\sigma^*(t_n))\]

We say that \(\phi\) is true under interpretation \({\cal M}\), when its free variables are given values according to assignment \(\sigma\), denoted by \({\cal M} \models \phi(\sigma)\), in the following cases:

• For any two terms \(t_1\), \(t_2\), \({\cal M} \models (t_1 = t_2)(\sigma)\) iff \(\sigma^*(t_1)\) and \(\sigma^*(t_2)\) are the same element.

• For any \(n\)-ary predicate symbol \(P\) and terms \(t_1,\ldots,t_n\) of appropiate type, \({\cal M} \models P(t_1,\ldots,t_n)(\sigma)\) iff \((\sigma^*(t_1),\ldots,\sigma^*(t_n)) \in P^{\cal M}\).

• \({\cal M} \models (\neg \phi)(\sigma)\) iff not \({\cal M} \models \phi\).

• If \(\phi \equiv \phi_1 \land \phi_2\), then \({\cal M} \models \phi(\sigma)\) iff \({\cal M} \models \phi_1\) and \({\cal M} \models \phi_2\).

• If \(\phi \equiv \phi_1 \lor \phi_2\), then \({\cal M} \models \phi(\sigma)\) iff \({\cal M} \models \phi_1\) or \({\cal M} \models \phi_2\).

• \({\cal M} \models (\exists_{\tau} x)(\sigma)\) iff \({\cal M} \models \phi(\sigma[x/a])\), for some \(a \in {\cal U}_\tau\).

• \({\cal M} \models (\forall_{\tau} x)(\sigma)\) iff \({\cal M} \models \phi(\sigma[x/a])\), for every \(a \in {\cal U}_\tau\).

where \(\sigma[x/a]\) is the function that assigns values as in \(\sigma\) except to variable \(x\), which is assigned the value \(a\).

Satisfaction and Validity

Definition (Satisfaction and Validity). Let \(\phi\) be a formula in some first-order language \({\cal L}\). We say that

• An interpretation \({\cal M}\) satisfies \(\phi\) iff \({\cal M} \models \phi(\sigma)\) for any possible assignment \(\sigma\). \(\phi\) is satisfiable iff there is some interpretation \({\cal M}\) that satisfies it.

• \(\phi\) is a valid formula, denoted \(\models \phi\), iff every possible first-order interpretation of \({\cal L}\) satisfies \(\phi\).

Determining if a first-order logic sentence \(\phi\) is valid is undecidable, and so it is determining that it is satisfiable.

The Semantics of the Languages Constructed with Tarski

As we have seen above, the semantics of a first–order language \({\cal L}\) are given by the interpretation \({\cal M}\). Informally, interpretations are sets of tables, relations and functions that map terms and formulas into objects and truth values. Tarski restricts languages to have one single interpretation, therefore, languages have associated a model which provides the semantics of built-in sorts and functional symbols.

We will next go over how Tarski implements interpretations \({\cal M}\).

Universes

Universes are defined in Tarski as one defines constants and associates them to a given sort. For the built-in sorts Real, Integer and Natural, this is done by default for each new language \({\cal L}\) defined. The construction routine associates with each of these sorts whatever is the range of real, integer and natural numbers that can be represented by the underlying hardware.

Universes of custom sorts are initially empty, so the statement

b1, b2, b3, b4 = [ bw.constant( 'b_{}'.format(k), block) for k in (1,2,3,4) ]

is setting the definition of universe \({\cal U}_{block}\) and \({\cal U}_{place}\) to be

\[{\cal U}_{block} = \{ b_1,\,b_2,\,\ldots,\,b_4 \} \cup {\cal U}_{block}\]

\[{\cal U}_{place} = \{ b_1,\,b_2,\,\ldots,\,b_4 \} \cup {\cal U}_{place}\]

as it is adding to \({\cal U}_{block}\) and \({\cal U}_{place}\) four objects. The latter is the result of having defined the sort block to be a subset of place, so therefore, every element of block is to be an element of place too. After the statement

table = bw.constant('table', place)

the universe \({\cal U}_{place}\) is made up of five objects

\[{\cal U}_{place} = \{ table \} \cup \{ b_1,\,b_2,\,\ldots,\,b_4 \}\]

We can check the definition of the universe of a given sort with the dump method

place.dump()

{'name': 'place', 'domain': ['b_2', 'b_1', 'table', 'b_3', 'b_4']}

where domain refers to the fact that free variables of sort place are allowed to be assigned exactly one of those values.

Giving Meaning to Function Symbols

For each function symbol \(f\) the model \({\cal M}\) of a language \({\cal L}\) keeps a dictionary, where each entry corresponds to a tuple of constants \((o_1,\ldots,o_n,o_{n+1})\) of types \(\tau_1,\ldots,\tau_n,\tau_{n+1}\). A new mapping can be specified with the add method of a Model object \(s\):

import tarski.model
import tarski.evaluators

s = tarski.model.create(bw)
s.evaluator = tarski.evaluators.get_entry_point('simple')

s.set( loc(b1), table)

so that the statement above is effectively equivalent to \(loc(b_1):=table\). The value associated to a given tuple of constants can be retrieved with Python’s standard [] operator

print(s[loc(b1)])

table

We will give now value to some more functional symbols

s.set(loc(b2), table) # block b2 is on the table
s.set(loc(b3), b2) # block b3 is on block 2
s.set(width(b1), 3.0) # block b1 has a width of 3.0 units
s.set(width(b2), 3.0) # block b2 has a width of 3.0 units
s.set(width(b3), 4.0) # block b3 has a width of 4.0 units

print(s[width(b1)])

3.0

Giving Meaning to Predicates

Tarski languages represent \(P^{\cal M}\) either extensionally, as tables of tuples of constants for which the predicate is defined, or intensionally as a procedure that maps a tuple of constants into either \(\top\) or \(\bot\).

We can add a new tuple of constants to the extension of predicate \(P\) using the method add

my_blocks = [ b1, b2, b3, b4]

for b in my_blocks :
    s.add(clear, b)

Evaluating the satisfiability of a predicate \(P\) under a given interpretation of its arguments can be done via the satisifed method

s[clear(b1)]

True

s[clear(b2)]

True

Relational Operators

Relational operators like \(>\), \(=\) etc. have standard, well defined meanings for sorts such as Real and its descendants (including Interval sorts). Tarski offers a wide variety of built-in predicates (and functions) to represent compactly arbitrarily complex arithmetic and algebraic expressions. Nevertheless, by default Tarski does not attach these definition to first order languages. It is required of the user to do this explicitly, as covered in this tutorial. For the purpose of illustrating the use of interpretations (models) let’s create the predicate leq

leq = bw.predicate('leq', bw.Real, bw.Real)

and we give meaning to it in the standard manner, for a few possible values

import numpy as np

---------------------------------------------------------------------------
ModuleNotFoundError                       Traceback (most recent call last)
/tmp/ipykernel_391/3593848235.py in <module>
----> 1 import numpy as np

ModuleNotFoundError: No module named 'numpy'

for x in np.arange(1.0,5.0):
    for y in np.arange(x, 5.0):
        s.add(leq, x, y)

---------------------------------------------------------------------------
NameError                                 Traceback (most recent call last)
/tmp/ipykernel_391/3891638196.py in <module>
----> 1 for x in np.arange(1.0,5.0):
      2     for y in np.arange(x, 5.0):
      3         s.add(leq, x, y)

NameError: name 'np' is not defined

Example: Nested functions for compact preconditions

Let us consider the case that we want to model Blocks World in such a way that the agent is required to look at a block before being able to pick it up, or to stack another block on top. For that we can introduce the 0-ary function

looking_at = bw.function('looking_at', block)
holding = bw.function('holding', block)

that maps into the sort block. We have also defined a function holding, to represent the block being hold by the agent. Their value on the interpretation s can be defined using the set() method

s.set( looking_at(), b2 )
s.set( holding(), b1)

The precondition of the stack action, requiring the block to be stacked to be smaller than the other one, at could then be modeled as follows

precondition = (leq(width(holding()), width(looking_at()))) & (clear(looking_at()))

which evaluates to True.

s[precondition]

False