propositions.semantics module

Semantic analysis of propositional-logic constructs.

propositions.semantics.Model

A model for propositional-logic formulas, a mapping from variable names to truth values.

alias of Mapping[str, bool]

propositions.semantics.is_model(model)

Checks if the given dictionary is a model over some set of variable names.

Parameters

model (Mapping[str, bool]) – dictionary to check.

Return type

bool

Returns

True if the given dictionary is a model over some set of variable names, False otherwise.

propositions.semantics.variables(model)

Finds all variable names over which the given model is defined.

Parameters

model (Mapping[str, bool]) – model to check.

Return type

AbstractSet[str]

Returns

A set of all variable names over which the given model is defined.

propositions.semantics.evaluate(formula, model)

Calculates the truth value of the given formula in the given model.

Parameters

  • formula (Formula) – formula to calculate the truth value of.

  • model (Mapping[str, bool]) – model over (possibly a superset of) the variable names of the given formula, to calculate the truth value in.

Return type

bool

Returns

The truth value of the given formula in the given model.

Examples

>>> evaluate(Formula.parse('~(p&q76)'), {'p': True, 'q76': False})
True

>>> evaluate(Formula.parse('~(p&q76)'), {'p': True, 'q76': True})
False
propositions.semantics.all_models(variables)

Calculates all possible models over the given variable names.

Parameters

variables (Sequence[str]) – variable names over which to calculate the models.

Return type

Iterable[Mapping[str, bool]]

Returns

An iterable over all possible models over the given variable names. The order of the models is lexicographic according to the order of the given variable names, where False precedes True.

Examples

>>> list(all_models(['p', 'q']))
[{'p': False, 'q': False}, {'p': False, 'q': True}, {'p': True, 'q': False}, {'p': True, 'q': True}]

>>> list(all_models(['q', 'p']))
[{'q': False, 'p': False}, {'q': False, 'p': True}, {'q': True, 'p': False}, {'q': True, 'p': True}]
propositions.semantics.truth_values(formula, models)

Calculates the truth value of the given formula in each of the given models.

Parameters

  • formula (Formula) – formula to calculate the truth value of.

  • models (Iterable[Mapping[str, bool]]) – iterable over models to calculate the truth value in.

Return type

Iterable[bool]

Returns

An iterable over the respective truth values of the given formula in each of the given models, in the order of the given models.

Examples

>>> list(truth_values(Formula.parse('~(p&q76)'), all_models(['p', 'q76'])))
[True, True, True, False]
propositions.semantics.print_truth_table(formula)

Prints the truth table of the given formula, with variable-name columns sorted alphabetically.

Parameters

formula (Formula) – formula to print the truth table of.

Examples

>>> print_truth_table(Formula.parse('~(p&q76)'))
| p | q76 | ~(p&q76) |
|---|-----|----------|
| F | F   | T        |
| F | T   | T        |
| T | F   | T        |
| T | T   | F        |
Return type

None

propositions.semantics.is_tautology(formula)

Checks if the given formula is a tautology.

Parameters

formula (Formula) – formula to check.

Return type

bool

Returns

True if the given formula is a tautology, False otherwise.

propositions.semantics.is_contradiction(formula)

Checks if the given formula is a contradiction.

Parameters

formula (Formula) – formula to check.

Return type

bool

Returns

True if the given formula is a contradiction, False otherwise.

propositions.semantics.is_satisfiable(formula)

Checks if the given formula is satisfiable.

Parameters

formula (Formula) – formula to check.

Return type

bool

Returns

True if the given formula is satisfiable, False otherwise.

propositions.semantics._synthesize_for_model(model)

Synthesizes a propositional formula in the form of a single conjunctive clause that evaluates to True in the given model, and to False in any other model over the same variable names.

Parameters

model (Mapping[str, bool]) – model over a nonempty set of variable names, in which the synthesized formula is to hold.

Return type

Formula

Returns

The synthesized formula.

propositions.semantics.synthesize(variables, values)

Synthesizes a propositional formula in DNF over the given variable names, that has the specified truth table.

Parameters

  • variables (Sequence[str]) – nonempty set of variable names for the synthesized formula.

  • values (Iterable[bool]) – iterable over truth values for the synthesized formula in every possible model over the given variable names, in the order returned by all_models(variables).

Return type

Formula

Returns

The synthesized formula.

Examples

>>> formula = synthesize(['p', 'q'], [True, True, True, False])
>>> for model in all_models(['p', 'q']):
...     evaluate(formula, model)
True
True
True
False
propositions.semantics._synthesize_for_all_except_model(model)

Synthesizes a propositional formula in the form of a single disjunctive clause that evaluates to False in the given model, and to True in any other model over the same variable names.

Parameters

model (Mapping[str, bool]) – model over a nonempty set of variable names, in which the synthesized formula is to not hold.

Return type

Formula

Returns

The synthesized formula.

propositions.semantics.synthesize_cnf(variables, values)

Synthesizes a propositional formula in CNF over the given variable names, that has the specified truth table.

Parameters

  • variables (Sequence[str]) – nonempty set of variable names for the synthesized formula.

  • values (Iterable[bool]) – iterable over truth values for the synthesized formula in every possible model over the given variable names, in the order returned by all_models(variables).

Return type

Formula

Returns

The synthesized formula.

Examples

>>> formula = synthesize_cnf(['p', 'q'], [True, True, True, False])
>>> for model in all_models(['p', 'q']):
...     evaluate(formula, model)
True
True
True
False
propositions.semantics.evaluate_inference(rule, model)

Checks if the given inference rule holds in the given model.

Parameters
Return type

bool

Returns

True if the given inference rule holds in the given model, False otherwise.

Examples

>>> evaluate_inference(InferenceRule([Formula('p')], Formula('q')),
...                    {'p': True, 'q': False})
False

>>> evaluate_inference(InferenceRule([Formula('p')], Formula('q')),
...                    {'p': False, 'q': False})
True
propositions.semantics.is_sound_inference(rule)

Checks if the given inference rule is sound, i.e., whether its conclusion is a semantically correct implication of its assumptions.

Parameters

rule (InferenceRule) – inference rule to check.

Return type

bool

Returns

True if the given inference rule is sound, False otherwise.