predicates.syntax module¶
Syntactic handling of predicate-logic expressions.
-
exception
predicates.syntax.
ForbiddenVariableError
(variable_name)¶ Bases:
Exception
Raised by
Term.substitute
andFormula.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.
-
predicates.syntax.
is_variable
(string)¶ Checks if the given string is a variable name.
-
predicates.syntax.
is_function
(string)¶ Checks if the given string is a function name.
-
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
-
__repr__
()¶ Computes the string representation of the current term.
- Return type
- Returns
The standard string representation of the current term.
-
__eq__
(other)¶ Compares the current term with the given one.
-
__ne__
(other)¶ Compares the current term with the given one.
-
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
- 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.
-
constants
()¶ Finds all constant names in the current term.
-
variables
()¶ Finds all variable names in the current term.
-
functions
()¶ Finds all function names in the current term, along with their arities.
-
substitute
(substitution_map, forbidden_variables=frozenset({}))¶ Substitutes in the current term, each constant name
construct
or variable nameconstruct
that is a key insubstitution_map
with the termsubstitution_map
[
construct
]
.- Parameters
substitution_map (
Mapping
[str
,Term
]) – mapping defining the substitutions to be performed.forbidden_variables (
AbstractSet
[str
]) – variable names not allowed in substitution terms.
- Return type
- Returns
The term resulting from performing all substitutions. Only constant name and variable name occurrences 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 name 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.
-
predicates.syntax.
is_relation
(string)¶ Checks if the given string is a relation name.
-
predicates.syntax.
is_unary
(string)¶ Checks if the given string is a unary operator.
-
predicates.syntax.
is_binary
(string)¶ Checks if the given string is a binary operator.
-
predicates.syntax.
is_quantifier
(string)¶ Checks if the given string is a quantifier.
-
class
predicates.syntax.
Formula
(root, arguments_or_first_or_variable, second_or_statement=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 of the root, if the root is a relation name or the equality relation.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.variable (
Optional
[str
]) – the variable name quantified by the root, if the root is a quantification.statement (
Optional
[Formula
]) – the statement quantified by the root, if the root is a quantification.
-
__init__
(root, arguments_or_first_or_variable, second_or_statement=None)¶ Initializes a
Formula
from its root and root arguments, root operands, or root quantified variable name and statement.- Parameters
root (
str
) – the root for the formula tree.arguments_or_first_or_variable (
Union
[Sequence
[Term
],Formula
,str
]) – the arguments for the root, if the root is a relation name or the equality relation; the first operand for the root, if the root is a unary or binary operator; the variable name to be quantified by the root, if the root is a quantification.second_or_statement (
Optional
[Formula
]) – the second operand for the root, if the root is a binary operator; the statement to be quantified by the root, if the root is a quantification.
-
__repr__
()¶ Computes the string representation of the current formula.
- Return type
- Returns
The standard string representation of the current formula.
-
__eq__
(other)¶ Compares the current formula with the given one.
-
__ne__
(other)¶ Compares the current formula with the given one.
-
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
- 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.,
'f(y)=c12'
) or by a variable name (e.g.,'f(y)=x12'
), then the parsed prefix will include that entire name (and not just a part of it, such as'f(y)=x1'
).
-
static
parse
(string)¶ Parses the given valid string representation into a formula.
-
constants
()¶ Finds all constant names in the current formula.
-
variables
()¶ Finds all variable names in the current formula.
-
free_variables
()¶ Finds all variable names that are free in the current formula.
-
functions
()¶ Finds all function names in the current formula, along with their arities.
-
relations
()¶ Finds all relation names in the current formula, along with their arities.
-
substitute
(substitution_map, forbidden_variables=frozenset({}))¶ Substitutes in the current formula, each constant name
construct
or free occurrence of variable nameconstruct
that is a key insubstitution_map
with the termsubstitution_map
[
construct
]
.- Parameters
substitution_map (
Mapping
[str
,Term
]) – mapping defining the substitutions to be performed.forbidden_variables (
AbstractSet
[str
]) – variable names not allowed in substitution terms.
- Return type
- Returns
The formula resulting from performing all substitutions. Only constant name and variable name occurrences 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 name from
forbidden_variables
or a variable name 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
- 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 name, equality, or quantifier at its root with a propositional variable name, consistently such that multiple identical such (outermost) subformulas are substituted with the same propositional variable name. The propositional variable names used for substitution are obtained, from left to right (considering their first occurrence), by calling
next
(
fresh_variable_name_generator
)
. The second element of the pair is a mapping from each propositional variable name to the subformula for which it was substituted.
Examples
>>> formula = Formula.parse('((Ax[x=7]&x=7)|(~Q(y)->x=7))') >>> formula.propositional_skeleton() (((z1&z2)|(~z3->z2)), {'z1': Ax[x=7], 'z2': x=7, 'z3': Q(y)}) >>> formula.propositional_skeleton() (((z4&z5)|(~z6->z5)), {'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
- Return type
- Returns
A predicate-logic formula obtained from the given propositional skeleton by substituting each propositional variable name with the formula mapped to it by the given map.
Examples
>>> Formula.from_propositional_skeleton( ... PropositionalFormula.parse('((z1&z2)|(~z3->z2))'), ... {'z1': Formula.parse('Ax[x=7]'), 'z2': Formula.parse('x=7'), ... 'z3': Formula.parse('Q(y)')}) ((Ax[x=7]&x=7)|(~Q(y)->x=7))
>>> Formula.from_propositional_skeleton( ... PropositionalFormula.parse('((z9&z2)|(~z3->z2))'), ... {'z2': Formula.parse('x=7'), 'z3': Formula.parse('Q(y)'), ... 'z9': Formula.parse('Ax[x=7]')}) ((Ax[x=7]&x=7)|(~Q(y)->x=7))