predicates.semantics module

Semantic analysis of predicate-logic 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 predicate-logic 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 to -1 if the relation is the empty relation.

  • relation_meanings (Mapping[str, AbstractSet[Tuple[T, …]]]) – mapping from each n-ary relation name to argument n-tuples (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 n-ary function name to the mapping from each argument n-tuple (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 n-ary relation, to the argument n-tuples (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 n-ary function, to a mapping from each argument n-tuple (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

str

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
  • term (Term) – term to calculate the value of, for the constants and functions of which the current model has meanings.

  • assignment (Mapping[str, ~T]) – mapping from each variable name in the given term to a universe element to which it is to be evaluated.

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

bool

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

bool

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.