# 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 variables.

Parameters

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

Return type

`bool`

Returns

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

`propositions.semantics.``variables`(model)

Finds all variables over which the given model is defined.

Parameters

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

Return type
Returns

A set of all variables 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
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 variables.

Parameters

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

Return type
Returns

An iterable over all possible models over the given variables. The order of the models is lexicographic according to the order of the given variables, 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 model.

Parameters
Return type
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 variables.

Parameters

model (`Mapping`[`str`, `bool`]) – model over a nonempty set of variables, 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 variables, that has the specified truth table.

Parameters
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 variables.

Parameters

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

Return type

`Formula`

Returns

The synthesized formula.

`propositions.semantics.``synthesize_cnf`(variables, values)

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

Parameters
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.