propositions.syntax module¶

Syntactic handling of propositional formulas.

propositions.syntax.is_variable(string)¶

Checks if the given string is a variable name.

Parameters: string (str) – string to check.
Return type: bool
Returns: True if the given string is a variable name, 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 variable names, and operators applied to them.

Variables

root (str) – the constant, variable name, or operator at the root of the formula tree.
first (Optional[Formula]) – the first operand of the root, if the root is a unary or binary operator.
second (Optional[Formula]) – the second operand of 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 for the root, if the root is a unary or binary operator.
second (Optional[Formula]) – the second operand for 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 variable names in the current formula.

Return type: Set[str]
Returns: A set of all variable names 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 followed 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 name 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 variable name occurrences originating in the current formula are substituted (i.e., variable name occurrences 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 operator occurrences originating in the current formula are substituted (i.e., operator occurrences 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)