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)))