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