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_meanings, relation_meanings, function_meanings={})¶ 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_meanings (
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 the arity of the relation, or to1
if the relation is the empty relation.relation_meanings (
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 the arity of the function.function_meanings (
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_meanings, relation_meanings, function_meanings={})¶ Initializes a
Model
from its universe and constant, relation, and function meanings. Parameters
universe (
AbstractSet
[~T]) – the set of elements to which terms are to be evaluated and over which quantifications are to be defined.constant_meanings (
Mapping
[str
, ~T]) – mapping from each constant name to a universe element to which it is to be evaluated.relation_meanings (
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_meanings (
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, for the given assignment of values to variables names.
 Parameters
 Return type
~T
 Returns
The value (in the universe of the current model) of the given term in the current model, for the given assignment of values to variable names.

evaluate_formula
(formula, assignment={})¶ Calculates the truth value of the given formula in the current model, for the given assignment of values to free occurrences of variables names.
 Parameters
formula (
Formula
) – formula to calculate the truth value of, for the constants, functions, and relations of which the current model has meanings.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, for the given assignment of values to free occurrences of variable names.

is_model_of
(formulas)¶ Checks if the current model is a model for the given formulas.
 Return type
 Returns
True
if each of the given formulas evaluates to true in the current model for any assignment of elements from the universe of the current model to the free occurrences of variables in that formula,False
otherwise.