propositions.syntax module

Syntactic handling of propositional formulas.

propositions.syntax.is_variable(string)

Checks if the given string is an atomic proposition.

Parameters

string (str) – string to check.

Return type

bool

Returns

True if the given string is an atomic proposition, False otherwise.

propositions.syntax.is_constant(string)

Checks if the given string is a constant.

Parameters

string (str) – string to check.

Return type

bool

Returns

True if the given string is a constant, False otherwise.

propositions.syntax.is_unary(string)

Checks if the given string is a unary operator.

Parameters

string (str) – string to check.

Return type

bool

Returns

True if the given string is a unary operator, False otherwise.

propositions.syntax.is_binary(string)

Checks if the given string is a binary operator.

Parameters

string (str) – string to check.

Return type

bool

Returns

True if the given string is a binary operator, False otherwise.

class propositions.syntax.Formula(root, first=None, second=None)

Bases: object

An immutable propositional formula in tree representation, composed from atomic propositions, and operators applied to them.

Variables
  • root (str) – the constant, atomic proposition, or operator at the root of the formula tree.

  • first (Optional[Formula]) – the first operand to the root, if the root is a unary or binary operator.

  • second (Optional[Formula]) – the second operand to the root, if the root is a binary operator.

__init__(root, first=None, second=None)

Initializes a Formula from its root and root operands.

Parameters
  • root (str) – the root for the formula tree.

  • first (Optional[Formula]) – the first operand to the root, if the root is a unary or binary operator.

  • second (Optional[Formula]) – the second operand to the root, if the root is a binary operator.

__repr__()

Computes the string representation of the current formula.

Return type

str

Returns

The standard string representation of the current formula.

__eq__(other)

Compares the current formula with the given one.

Parameters

other (object) – object to compare to.

Return type

bool

Returns

True if the given object is a Formula object that equals the current formula, False otherwise.

__ne__(other)

Compares the current formula with the given one.

Parameters

other (object) – object to compare to.

Return type

bool

Returns

True if the given object is not a Formula object or does not equal the current formula, False otherwise.

variables()

Finds all atomic propositions (variables) in the current formula.

Return type

Set[str]

Returns

A set of all atomic propositions used in the current formula.

operators()

Finds all operators in the current formula.

Return type

Set[str]

Returns

A set of all operators (including 'T' and 'F') used in the current formula.

static _parse_prefix(string)

Parses a prefix of the given string into a formula.

Parameters

string (str) – string to parse.

Return type

Tuple[Optional[Formula], str]

Returns

A pair of the parsed formula and the unparsed suffix of the string. If the given string has as a prefix a variable name (e.g., 'x12') or a unary operator follows by a variable name, then the parsed prefix will include that entire variable name (and not just a part of it, such as 'x1'). If no prefix of the given string is a valid standard string representation of a formula then returned pair should be of None and an error message, where the error message is a string with some human-readable content.

static is_formula(string)

Checks if the given string is a valid representation of a formula.

Parameters

string (str) – string to check.

Return type

bool

Returns

True if the given string is a valid standard string representation of a formula, False otherwise.

static parse(string)

Parses the given valid string representation into a formula.

Parameters

string (str) – string to parse.

Return type

Formula

Returns

A formula whose standard string representation is the given string.

polish()

Computes the polish notation representation of the current formula.

Return type

str

Returns

The polish notation representation of the current formula.

static parse_polish(string)

Parses the given polish notation representation into a formula.

Parameters

string (str) – string to parse.

Return type

Formula

Returns

A formula whose polish notation representation is the given string.

substitute_variables(substitution_map)

Substitutes in the current formula, each variable v that is a key in substitution_map with the formula substitution_map[v].

Parameters

substitution_map (Mapping[str, Formula]) – mapping defining the substitutions to be performed.

Return type

Formula

Returns

The formula resulting from performing all substitutions. Only variables originating in the current formula are substituted (i.e., variables originating in one of the specified substitutions are not subjected to additional substitutions).

Examples

>>> Formula.parse('((p->p)|r)').substitute_variables(
...     {'p': Formula.parse('(q&r)'), 'r': Formula.parse('p')})
(((q&r)->(q&r))|p)
substitute_operators(substitution_map)

Substitutes in the current formula, each constant or operator op that is a key in substitution_map with the formula substitution_map[op] applied to its (zero or one or two) operands, where the first operand is used for every occurrence of 'p' in the formula and the second for every occurrence of 'q'.

Parameters

substitution_map (Mapping[str, Formula]) – mapping defining the substitutions to be performed.

Return type

Formula

Returns

The formula resulting from performing all substitutions. Only operators originating in the current formula are substituted (i.e., operators originating in one of the specified substitutions are not subjected to additional substitutions).

Examples

>>> Formula.parse('((x&y)&~z)').substitute_operators(
...     {'&': Formula.parse('~(~p|~q)')})
~(~~(~x|~y)|~~z)