predicates.semantics module¶
Semantic analysis of predicatelogic expressions.

predicates.semantics.
T
¶ A generic type for a universe element in a model.
alias of TypeVar(‘T’)

class
predicates.semantics.
Model
(universe, constant_interpretations, relation_interpretations, function_interpretations={})¶ Bases:
typing.Generic
An immutable model for predicatelogic constructs.
 Variables
universe (
FrozenSet
[T
]) – the set of elements to which terms can be evaluated and over which quantifications are defined.constant_interpretations (
Mapping
[str
,T
]) – mapping from each constant name to the universe element to which it evaluates.relation_arities (
Mapping
[str
,int
]) – mapping from each relation name to its arity, or to1
if the relation is the empty relation.relation_interpretations (
Mapping
[str
,AbstractSet
[Tuple
[T
, …]]]) – mapping from each nary relation name to argument ntuples (of universe elements) for which the relation is true.function_arities (
Mapping
[str
,int
]) – mapping from each function name to its arity.function_interpretations (
Mapping
[str
,Mapping
[Tuple
[T
, …],T
]]) – mapping from each nary function name to the mapping from each argument ntuple (of universe elements) to the universe element that the function outputs given these arguments.

__init__
(universe, constant_interpretations, relation_interpretations, function_interpretations={})¶ Initializes a
Model
from its universe and constant, relation, and function name interpretations. Parameters
universe (
AbstractSet
[~T]) – the set of elements to which terms are to be evaluated and over which quantifications are to be defined.constant_interpretations (
Mapping
[str
, ~T]) – mapping from each constant name to a universe element to which it is to be evaluated.relation_interpretations (
Mapping
[str
,AbstractSet
[Tuple
[~T, …]]]) – mapping from each relation name that is to be the name of an nary relation, to the argument ntuples (of universe elements) for which the relation is to be true.function_interpretations (
Mapping
[str
,Mapping
[Tuple
[~T, …], ~T]]) – mapping from each function name that is to be the name of an nary function, to a mapping from each argument ntuple (of universe elements) to a universe element that the function is to output given these arguments.

__repr__
()¶ Computes a string representation of the current model.
 Return type
 Returns
A string representation of the current model.

evaluate_term
(term, assignment={})¶ Calculates the value of the given term in the current model under the given assignment of values to variable names.
 Parameters
 Return type
~T
 Returns
The value (in the universe of the current model) of the given term in the current model under the given assignment of values to variable names.

evaluate_formula
(formula, assignment={})¶ Calculates the truth value of the given formula in the current model under the given assignment of values to free occurrences of variable names.
 Parameters
formula (
Formula
) – formula to calculate the truth value of, for the constant, function, and relation names of which the current model has interpretations.assignment (
Mapping
[str
, ~T]) – mapping from each variable name that has a free occurrence in the given formula to a universe element to which it is to be evaluated.
 Return type
 Returns
The truth value of the given formula in the current model under the given assignment of values to free occurrences of variable names.

is_model_of
(formulas)¶ Checks if the current model is a model of the given formulas.
 Parameters
formulas (
AbstractSet
[Formula
]) – formulas to check, for the constant, function, and relation names of which the current model has interpretations. Return type
 Returns
True
if each of the given formulas evaluates to true in the current model under any assignment of elements from the universe of the current model to the free occurrences of variable names in that formula,False
otherwise.