The Tarski API

class tarski.fol.FirstOrderLanguage(name=None)

A many-sorted first-order language.

property Boolean

A shorthand accessor for the Boolean sort.

property Integer

A shorthand accessor for the Integer sort.

property Natural

A shorthand accessor for the Natural sort.

property Object

A shorthand accessor for the object sort.

property Real

A shorthand accessor for the Real sort.

attach_sort(sort: tarski.syntax.sorts.Sort, parent: tarski.syntax.sorts.Sort)

Attach a given sort to the language. For standard creation of sorts, better use lang.sort().

constant(name: str, sort: Union[tarski.syntax.sorts.Sort, str])

Create a constant symbol with the specified sort, which can be given as a Sort object or as its name, if a Sort with that name has already been registered.

deepcopy()

Use this method instead of copy.deepcopy() if you need a true deep-copy of the language

get(first, *args)

Return the language element with given name(s). This can be a predicate or function symbol, including constants, or a sort name. Multiple names can be used to get different elements in one single call:

>>> lang = FirstOrderLanguage()
>>> lang.predicate('on', lang.get_sort('object'))
>>> lang.function('loc', lang.get_sort('object'), lang.get_sort('object'))
>>> on, loc = lang.get("on", "loc")
interval(name, parent: tarski.syntax.sorts.Interval, lower_bound, upper_bound)

Create a (bound) interval sort.

We allow only the new sort to derive from the built-in natural, integer or real sorts.

property ns

A helper to access the FOL symbols in an elegant and easy manner, to be used e.g. as in:

>>> lang = FirstOrderLanguage()
>>> lang.predicate('on', lang.get_sort('object'))
>>> print(f'The predicate object "on" is: {lang.ns.on}')

The overall idea is that the ns attribute (for “namespace”) encapsulates access to only the symbols in the first-order language (sorts, predicate and function symbols, including constants), and nothing else (that is, it knows nothing about other class methods and attributes).

sort(name: str, parent: Optional[Union[tarski.syntax.sorts.Sort, str]] = None)

Create new sort with given name and parent sort. The parent sort can be given as a Sort object or as its name, if a Sort with that name has already been registered. If no parent is specified, the “object” sort is assumed as parent.

Raises
  • err.DuplicateSortDefinition – if a sort with the same name already existed.

  • err.DuplicateDefinition – f some non-sort element with the same name already existed.

variable(name: str, sort: Union[tarski.syntax.sorts.Sort, str])

Create a variable symbol with the specified sort, which can be given as a Sort object or as its name, if a Sort with that name has already been registered.

vocabulary()

Return the vocabulary corresponding to this language. This is a triple with the signatures of, resp., predicates, functions and constants of the language.