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.