# 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:

```
[1]:
```

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

```
[1]:
```

```
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.

```
[2]:
```

```
lang.sorts
```

```
[2]:
```

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

```
[3]:
```

```
lang.predicates
```

```
[3]:
```

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

```
[4]:
```

```
lang.functions
```

```
[4]:
```

```
[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:

```
[5]:
```

```
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”):

```
[6]:
```

```
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:

```
[7]:
```

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

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

```
[8]:
```

```
lang.constants()
```

```
[8]:
```

```
[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:

```
[9]:
```

```
lang.get_sort('place')
```

```
[9]:
```

```
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:

```
[10]:
```

```
lang.constant(3, lang.Real)
```

```
[10]:
```

```
3.0 (Real)
```

```
[11]:
```

```
lang.constant(42, lang.Integer)
```

```
[11]:
```

```
42 (Integer)
```

or even

```
[12]:
```

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

```
---------------------------------------------------------------------------
ModuleNotFoundError Traceback (most recent call last)
<ipython-input-1-f0f6351f7a5c> 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:

```
[13]:
```

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

And can be easily distinguished because of their attribute `builtin`

:

```
[14]:
```

```
lang.Real.builtin
```

```
[14]:
```

```
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

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

```
[15]:
```

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

Constants are then given as in the unrestricted case

```
[16]:
```

```
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

```
[17]:
```

```
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\)

```
[18]:
```

```
alpha = lang.sort('alpha')
```

```
[19]:
```

```
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`

```
[20]:
```

```
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

```
[21]:
```

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

```
Parent of Sort(Real) is Sort(object)
```

```
[22]:
```

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

```
Parent of Sort(Integer) is Sort(Real)
```

```
[23]:
```

```
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

```
[24]:
```

```
import tarski
import tarski.errors as err
```

```
[25]:
```

```
bw = tarski.language()
```

Blocks Worlds are made of objects of two sorts:

```
[26]:
```

```
place = bw.sort('place')
```

and

```
[27]:
```

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

We populate our instance with a few blocks

```
[28]:
```

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

and a table

```
[29]:
```

```
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

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

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

```
[30]:
```

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

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

```
[31]:
```

```
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*.

```
[32]:
```

```
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

```
[33]:
```

```
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

```
[34]:
```

```
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

```
[35]:
```

```
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

```
[36]:
```

```
# 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`

```
[37]:
```

```
from tarski import Term
isinstance(b1,Term)
```

```
[37]:
```

```
True
```

Function symbols allow to nest terms, thus

```
[38]:
```

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

```
[38]:
```

```
True
```

```
[39]:
```

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

```
[39]:
```

```
True
```

```
[40]:
```

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

```
[40]:
```

```
True
```

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

```
[41]:
```

```
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

```
[42]:
```

```
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

```
[43]:
```

```
str(tau)
```

```
[43]:
```

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

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

```
[44]:
```

```
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*

which can be written as

```
[45]:
```

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

which is represented internally

```
[46]:
```

```
str(phi)
```

```
[46]:
```

```
'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

was transformed into the disjunction

using the transformation

We can use the operator `>`

instead of the function `implies()`

, if a more concise syntax is preferred.

```
[47]:
```

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

We can write the conjunctive formula

in several ways. One is using the `land`

function

```
[48]:
```

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

or the operator `&`

```
[49]:
```

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

Another state invariant like

can be written as

```
[50]:
```

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

or

```
[51]:
```

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

Finally, the formula

can be written as

```
[52]:
```

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

```
[52]:
```

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

or, alternatively the `~`

unary operator can be used instead of `neg`

```
[53]:
```

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

```
[53]:
```

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

## Semantics of First-Order Languages¶

```
[54]:
```

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

```
[55]:
```

```
# 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

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:

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

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

```
[56]:
```

```
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

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

```
[57]:
```

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

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

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

method

```
[58]:
```

```
place.dump()
```

```
[58]:
```

```
{'name': 'place', 'domain': ['b_1', 'b_3', 'b_2', 'table', '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\):

```
[59]:
```

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

```
[60]:
```

```
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

```
[61]:
```

```
print(s[loc(b1)])
```

```
table
```

We will give now value to some more functional symbols

```
[62]:
```

```
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
```

```
[63]:
```

```
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`

```
[64]:
```

```
my_blocks = [ b1, b2, b3, b4]
```

```
[65]:
```

```
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

```
[66]:
```

```
s[clear(b1)]
```

```
[66]:
```

```
True
```

```
[67]:
```

```
s[clear(b2)]
```

```
[67]:
```

```
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`

```
[68]:
```

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

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

```
[69]:
```

```
import numpy as np
```

```
---------------------------------------------------------------------------
ModuleNotFoundError Traceback (most recent call last)
<ipython-input-1-0aa0b027fcb6> in <module>
----> 1 import numpy as np
ModuleNotFoundError: No module named 'numpy'
```

```
[70]:
```

```
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)
<ipython-input-1-102be7f629d3> 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

```
[71]:
```

```
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

```
[72]:
```

```
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

```
[73]:
```

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

which evaluates to `True`

.

```
[74]:
```

```
s[precondition]
```

```
[74]:
```

```
False
```