# Advanced Problem Definition Techniques [WORK IN PROGRESS]¶

## Using Theories¶

:

import tarski

# 1. Create language equipped with the Arithmetic theory
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)

:

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

:

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

:

import tarski.model
import tarski.evaluators

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

:

s.set( loc(b1), table)

:

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


## Built-in Function Symbols¶

A number of functions are already defined for the built-in sorts Real, Integer and Natural, in order to facilitate the definition of terms that model arithmetic operators, algebraic and transcendental functions

Name

Syntax

Notes

Name

Syntax

Notes

x + y

Power

x ** y

Subtraction

x - y

Multiplication

x * y

Division

x / y

Modulo

x % y

### Examples¶

We can write crazy stuff like:

:

expr1 = width(b1) + width(b2)

:

print(expr1)

+(width(b_1), width(b_2))

:

expr2 = width(b1) * width(b2)

:

print(expr2)

*(width(b_1), width(b_2))


and evaluate it with the $$\sigma$$ operator, which is implemented by the eval method of our language

:

s[expr1]

:

6.0 (Real)

:

s[expr2]

:

9.0 (Real)


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


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

:

print(s[clear(b1)])

True

:

print(s[clear(b2)])

True


Relational operators like $$>$$, $$=$$ etc. are represented always procedurally when the sorts of the arguments are built-in sorts such as Real.

NB: It may be interesting to highlight that predicates are actually constraints that we use to define states.

## Formula evaluation¶

### Example: Nested functions for compact preconditions¶

:

looking_at = bw.function('looking_at', block)
s.set(looking_at(), b1)
precondition = (width(looking_at()) <= width(b2)) & (clear(b2))
s[precondition]

:

True