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().
-
connected_in_type_hierarchy
(t_0, t_goal)¶ Checks if there is a path in the type hierarchy between t_0 and t_goal :param t_0: :param t_goal: :return:
-
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.
-
property