predicates.syntax module¶

Syntactic handling of predicate-logic expressions.

exception predicates.syntax.ForbiddenVariableError(variable_name)¶

Bases: Exception

Raised by Term.substitute and Formula.substitute when a substituted term contains a variable name that is forbidden in that context.

Variables: variable_name (str) – the variable name that was forbidden in the context in which a term containing it was to be substituted.

__init__(variable_name)¶

Initializes a ForbiddenVariableError from the offending variable name.

Parameters: variable_name (str) – variable name that is forbidden in the context in which a term containing it is to be substituted.

predicates.syntax.is_constant(string)¶

Checks if the given string is a constant name.

Parameters: string (str) – string to check.
Return type: bool
Returns: True if the given string is a constant name, False otherwise.

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

predicates.syntax.is_function(string)¶

Checks if the given string is a function name.

Parameters: string (str) – string to check.
Return type: bool
Returns: True if the given string is a function name, False otherwise.

class predicates.syntax.Term(root, arguments=None)¶

Bases: object

An immutable predicate-logic term in tree representation, composed from variable names and constant names, and function names applied to them.

Variables

root (str) – the constant name, variable name, or function name at the root of the term tree.
arguments (Optional[Tuple[Term, …]]) – the arguments to the root, if the root is a function name.

__init__(root, arguments=None)¶

Initializes a Term from its root and root arguments.

Parameters

root (str) – the root for the formula tree.
arguments (Optional[Sequence[Term]]) – the arguments to the root, if the root is a function name.

__repr__()¶

Computes the string representation of the current term.

Return type: str
Returns: The standard string representation of the current term.

__eq__(other)¶

Compares the current term with the given one.

Parameters: other (object) – object to compare to.
Return type: bool
Returns: True if the given object is a Term object that equals the current term, False otherwise.

__ne__(other)¶

Compares the current term with the given one.

Parameters: other (object) – object to compare to.
Return type: bool
Returns: True if the given object is not a Term object or does not equal the current term, False otherwise.

static _parse_prefix(string)¶

Parses a prefix of the given string into a term.

Parameters: string (str) – string to parse, which has a prefix that is a valid representation of a term.
Return type: Tuple[Term, str]
Returns: A pair of the parsed term and the unparsed suffix of the string. If the given string has as a prefix a constant name (e.g., 'c12') or a variable name (e.g., 'x12'), then the parsed prefix will be that entire name (and not just a part of it, such as 'x1').

static parse(string)¶

Parses the given valid string representation into a term.

Parameters: string (str) – string to parse.
Return type: Term
Returns: A term whose standard string representation is the given string.

constants()¶

Finds all constant names in the current term.

Return type: Set[str]
Returns: A set of all constant names used in the current term.

variables()¶

Finds all variable names in the current term.

Return type: Set[str]
Returns: A set of all variable names used in the current term.

functions()¶

Finds all function names in the current term, along with their arities.

Return type: Set[Tuple[str, int]]
Returns: A set of pairs of function name and arity (number of arguments) for all function names used in the current term.

substitute(substitution_map, forbidden_variables=frozenset({}))¶

Substitutes in the current term, each constant name name or variable name name that is a key in substitution_map with the term substitution_map[name].

Parameters

substitution_map (Mapping[str, Term]) – mapping defining the substitutions to be performed.
forbidden_variables (AbstractSet[str]) – variables not allowed in substitution terms.

Return type

Term

Returns

The term resulting from performing all substitutions. Only constant names and variable names originating in the current term are substituted (i.e., those originating in one of the specified substitutions are not subjected to additional substitutions).

Raises

ForbiddenVariableError – If a term that is used in the requested substitution contains a variable from forbidden_variables.

Examples

>>> Term.parse('f(x,c)').substitute(
...     {'c': Term.parse('plus(d,x)'), 'x': Term.parse('c')}, {'y'})
f(c,plus(d,x))

>>> Term.parse('f(x,c)').substitute(
...     {'c': Term.parse('plus(d,y)')}, {'y'})
Traceback (most recent call last):
  ...
predicates.syntax.ForbiddenVariableError: y

predicates.syntax.is_equality(string)¶

Checks if the given string is the equality relation.

Parameters: string (str) – string to check.
Return type: bool
Returns: True if the given string is the equality relation, False otherwise.

predicates.syntax.is_relation(string)¶

Checks if the given string is a relation name.

Parameters: string (str) – string to check.
Return type: bool
Returns: True if the given string is a relation name, False otherwise.

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

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

predicates.syntax.is_quantifier(string)¶

Checks if the given string is a quantifier.

Parameters: string (str) – string to check.
Return type: bool
Returns: True if the given string is a quantifier, False otherwise.

class predicates.syntax.Formula(root, arguments_or_first_or_variable, second_or_predicate=None)¶

Bases: object

An immutable predicate-logic formula in tree representation, composed from relation names applied to predicate-logic terms, and operators and quantifications applied to them.

Variables

root (str) – the relation name, equality relation, operator, or quantifier at the root of the formula tree.
arguments (Optional[Tuple[Term, …]]) – the arguments to the root, if the root is a relation name or the equality relation.
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.
variable (Optional[str]) – the variable name quantified by the root, if the root is a quantification.
predicate (Optional[Formula]) – the predicate quantified by the root, if the root is a quantification.

__init__(root, arguments_or_first_or_variable, second_or_predicate=None)¶

Initializes a Formula from its root and root arguments, root operands, or root quantified variable and predicate.

Parameters

root (str) – the root for the formula tree.
arguments_or_first_or_variable (Union[Sequence[Term], Formula, str]) – the arguments to the root, if the root is a relation name or the equality relation; the first operand to the root, if the root is a unary or binary operator; the variable name quantified by the root, if the root is a quantification.
second_or_predicate (Optional[Formula]) – the second operand to the root, if the root is a binary operator; the predicate quantified by the root, if the root is a quantification.

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

static _parse_prefix(string)¶

Parses a prefix of the given string into a formula.

Parameters: string (str) – string to parse, which has a prefix that is a valid representation of a formula.
Return type: Tuple[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 term followed by an equality followed by a constant name (e.g., 'c12') or by a variable name (e.g., 'x12'), then the parsed prefix will include that entire name (and not just a part of it, such as 'x1').

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.

constants()¶

Finds all constant names in the current formula.

Return type: Set[str]
Returns: A set of all constant names used in the current formula.

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.

free_variables()¶

Finds all variable names that are free in the current formula.

Return type: Set[str]
Returns: A set of every variable name that is used in the current formula not only within a scope of a quantification on that variable name.

functions()¶

Finds all function names in the current formula, along with their arities.

Return type: Set[Tuple[str, int]]
Returns: A set of pairs of function name and arity (number of arguments) for all function names used in the current formula.

relations()¶

Finds all relation names in the current formula, along with their arities.

Return type: Set[Tuple[str, int]]
Returns: A set of pairs of relation name and arity (number of arguments) for all relation names used in the current formula.

substitute(substitution_map, forbidden_variables=frozenset({}))¶

Substitutes in the current formula, each constant name name or free occurrence of variable name name that is a key in substitution_map with the term substitution_map[name].

Parameters

substitution_map (Mapping[str, Term]) – mapping defining the substitutions to be performed.
forbidden_variables (AbstractSet[str]) – variables not allowed in substitution terms.

Return type

Formula

Returns

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

Raises

ForbiddenVariableError – If a term that is used in the requested substitution contains a variable from forbidden_variables or a variable occurrence that becomes bound when that term is substituted into the current formula.

Examples

>>> Formula.parse('Ay[x=c]').substitute(
...     {'c': Term.parse('plus(d,x)'), 'x': Term.parse('c')}, {'z'})
Ay[c=plus(d,x)]

>>> Formula.parse('Ay[x=c]').substitute(
...     {'c': Term.parse('plus(d,z)')}, {'z'})
Traceback (most recent call last):
  ...
predicates.syntax.ForbiddenVariableError: z

>>> Formula.parse('Ay[x=c]').substitute(
...     {'c': Term.parse('plus(d,y)')})
Traceback (most recent call last):
  ...
predicates.syntax.ForbiddenVariableError: y

propositional_skeleton()¶

Computes a propositional skeleton of the current formula.

Return type: Tuple[Formula, Mapping[str, Formula]]
Returns: A pair. The first element of the pair is a propositional formula obtained from the current formula by substituting every (outermost) subformula that has a relation or quantifier at its root with an atomic propositional formula, consistently such that multiple equal such (outermost) subformulas are substituted with the same atomic propositional formula. The atomic propositional formulas used for substitution are obtained, from left to right, by calling next(fresh_variable_name_generator). The second element of the pair is a mapping from each atomic propositional formula to the subformula for which it was substituted.

Examples

>>> formula = Formula.parse('((Ax[x=7]&x=7)|(x=7->~Q(y)))')
>>> formula.propositional_skeleton()
(((z1&z2)|(z2->~z3)), {'z1': Ax[x=7], 'z2': x=7, 'z3': Q(y)})
>>> formula.propositional_skeleton()
(((z4&z5)|(z5->~z6)), {'z4': Ax[x=7], 'z5': x=7, 'z6': Q(y)})

static from_propositional_skeleton(skeleton, substitution_map)¶

Computes a predicate-logic formula from a propositional skeleton and a substitution map.

Parameters

skeleton (Formula) – propositional skeleton for the formula to compute, containing no constants or operators beyond '~', '->', '|', and '&'.
substitution_map (Mapping[str, Formula]) – mapping from each atomic propositional subformula of the given skeleton to a predicate-logic formula.

Return type

Formula

Returns

A predicate-logic formula obtained from the given propositional skeleton by substituting each atomic propositional subformula with the formula mapped to it by the given map.

Examples

>>> Formula.from_propositional_skeleton(
...     PropositionalFormula.parse('((z1&z2)|(z2->~z3))'),
...     {'z1': Formula.parse('Ax[x=7]'), 'z2': Formula.parse('x=7'),
...      'z3': Formula.parse('Q(y)')})
((Ax[x=7]&x=7)|(x=7->~Q(y)))