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

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