predicates.prenex module

Conversion of predicate-logic formulas into prenex normal form.

predicates.prenex.ADDITIONAL_QUANTIFICATION_AXIOMS = (Schema: ((~Ax[R(x)]->Ex[~R(x)])&(Ex[~R(x)]->~Ax[R(x)])) [templates: R, x], Schema: ((~Ex[R(x)]->Ax[~R(x)])&(Ax[~R(x)]->~Ex[R(x)])) [templates: R, x], Schema: (((Ax[R(x)]&Q())->Ax[(R(x)&Q())])&(Ax[(R(x)&Q())]->(Ax[R(x)]&Q()))) [templates: Q, R, x], Schema: (((Ex[R(x)]&Q())->Ex[(R(x)&Q())])&(Ex[(R(x)&Q())]->(Ex[R(x)]&Q()))) [templates: Q, R, x], Schema: (((Q()&Ax[R(x)])->Ax[(Q()&R(x))])&(Ax[(Q()&R(x))]->(Q()&Ax[R(x)]))) [templates: Q, R, x], Schema: (((Q()&Ex[R(x)])->Ex[(Q()&R(x))])&(Ex[(Q()&R(x))]->(Q()&Ex[R(x)]))) [templates: Q, R, x], Schema: (((Ax[R(x)]|Q())->Ax[(R(x)|Q())])&(Ax[(R(x)|Q())]->(Ax[R(x)]|Q()))) [templates: Q, R, x], Schema: (((Ex[R(x)]|Q())->Ex[(R(x)|Q())])&(Ex[(R(x)|Q())]->(Ex[R(x)]|Q()))) [templates: Q, R, x], Schema: (((Q()|Ax[R(x)])->Ax[(Q()|R(x))])&(Ax[(Q()|R(x))]->(Q()|Ax[R(x)]))) [templates: Q, R, x], Schema: (((Q()|Ex[R(x)])->Ex[(Q()|R(x))])&(Ex[(Q()|R(x))]->(Q()|Ex[R(x)]))) [templates: Q, R, x], Schema: (((Ax[R(x)]->Q())->Ex[(R(x)->Q())])&(Ex[(R(x)->Q())]->(Ax[R(x)]->Q()))) [templates: Q, R, x], Schema: (((Ex[R(x)]->Q())->Ax[(R(x)->Q())])&(Ax[(R(x)->Q())]->(Ex[R(x)]->Q()))) [templates: Q, R, x], Schema: (((Q()->Ax[R(x)])->Ax[(Q()->R(x))])&(Ax[(Q()->R(x))]->(Q()->Ax[R(x)]))) [templates: Q, R, x], Schema: (((Q()->Ex[R(x)])->Ex[(Q()->R(x))])&(Ex[(Q()->R(x))]->(Q()->Ex[R(x)]))) [templates: Q, R, x], Schema: (((R(x)->Q(x))&(Q(x)->R(x)))->((Ax[R(x)]->Ay[Q(y)])&(Ay[Q(y)]->Ax[R(x)]))) [templates: Q, R, x, y], Schema: (((R(x)->Q(x))&(Q(x)->R(x)))->((Ex[R(x)]->Ey[Q(y)])&(Ey[Q(y)]->Ex[R(x)]))) [templates: Q, R, x, y])

Additional axioms of quantification for Predicate Logic.

predicates.prenex.is_quantifier_free(formula)

Checks if the given formula contains any quantifiers.

Parameters

formula (Formula) – formula to check.

Return type

bool

Returns

False if the given formula contains any quantifiers, True otherwise.

predicates.prenex.is_in_prenex_normal_form(formula)

Checks if the given formula is in prenex normal form.

Parameters

formula (Formula) – formula to check.

Return type

bool

Returns

True if the given formula in prenex normal form, False otherwise.

predicates.prenex.equivalence_of(formula1, formula2)

States the equivalence of the two given formulas as a formula.

Parameters
  • formula1 (Formula) – first of the formulas the equivalence of which is to be stated.

  • formula2 (Formula) – second of the formulas the equivalence of which is to be stated.

Return type

Formula

Returns

The formula '((formula1->formula2)&(formula2->formula1))'.

predicates.prenex.has_uniquely_named_variables(formula)

Checks if the given formula has uniquely named variables.

Parameters

formula (Formula) – formula to check.

Return type

bool

Returns

False if in the given formula some variable name has both quantified and free occurrences or is quantified by more than one quantifier, True otherwise.

Examples

>>> has_uniquely_named_variables(
...     Formula.parse('(x=0&(Ax[R(x)]|Ex[R(x)]))'))
False
>>> has_uniquely_named_variables(
...     Formula.parse('(x=0&(Ax[R(x)]|Ey[R(y)]))'))
False
>>> has_uniquely_named_variables(
...     Formula.parse('(y=0&(Ax[R(x)]|Ex[R(x)]))'))
False
>>> has_uniquely_named_variables(
...     Formula.parse('(x=0&(Ay[R(y)]|Ez[R(z)]))'))
True
predicates.prenex._uniquely_rename_quantified_variables(formula)

Converts the given formula to an equivalent formula with uniquely named variables, and proves the equivalence of these two formulas.

Parameters

formula (Formula) – formula to convert, which contains no variable names starting with z.

Return type

Tuple[Formula, Proof]

Returns

A pair. The first element of the pair is a formula equivalent to the given formula, with the exact same structure but with the additional property of having uniquely named variables, obtained by consistently replacing each variable name that is bound in the given formula with a new variable name obtained by calling next(fresh_variable_name_generator). The second element of the pair is a proof of the equivalence of the given formula and the returned formula (i.e., a proof of equivalence_of(formula,returned_formula)) via AXIOMS and ADDITIONAL_QUANTIFICATION_AXIOMS.

Examples

>>> formula = Formula.parse('~(w=x|Aw[(Ex[(x=w&Aw[w=x])]->Ax[x=y])])')
>>> returned_formula, proof = _uniquely_rename_quantified_variables(formula)
>>> returned_formula
~(w=x|Az58[(Ez17[(z17=z58&Az4[z4=z17])]->Az32[z32=y])])
>>> proof.is_valid()
True
>>> proof.conclusion == equivalence_of(formula, returned_formula)
True
>>> proof.assumptions == Prover.AXIOMS.union(
...     ADDITIONAL_QUANTIFICATION_AXIOMS)
True
predicates.prenex._pull_out_quantifications_across_negation(formula)

Converts the given formula with uniquely named variables of the form '~Q1x1[Q2x2[Qnxn[inner_formula]]]' to an equivalent formula of the form 'Q'1x1[Q'2x2[Q'nxn[~inner_formula]]]', and proves the equivalence of these two formulas.

Parameters

formula (Formula) – formula to convert, whose root is a negation, i.e., which is of the form '~Q1x1[Q2x2[Qnxn[inner_formula]]]' where n>=0, each Qi is a quantifier, each xi is a variable name, and inner_formula does not start with a quantifier.

Return type

Tuple[Formula, Proof]

Returns

A pair. The first element of the pair is a formula equivalent to the given formula, but of the form 'Q'1x1[Q'2x2[Q'nxn[~inner_formula]]]' where each Q'i is a quantifier, and where the xi variable names and inner_formula are the same as in the given formula. The second element of the pair is a proof of the equivalence of the given formula and the returned formula (i.e., a proof of equivalence_of(formula,returned_formula)) via AXIOMS and ADDITIONAL_QUANTIFICATION_AXIOMS.

Examples

>>> formula = Formula.parse('~Ax[Ey[R(x,y)]]')
>>> returned_formula, proof = _pull_out_quantifications_across_negation(
...     formula)
>>> returned_formula
Ex[Ay[~R(x,y)]]
>>> proof.is_valid()
True
>>> proof.conclusion == equivalence_of(formula, returned_formula)
True
>>> proof.assumptions == Prover.AXIOMS.union(
...     ADDITIONAL_QUANTIFICATION_AXIOMS)
True
predicates.prenex._pull_out_quantifications_from_left_across_binary_operator(formula)

Converts the given formula with uniquely named variables of the form '(Q1x1[Q2x2[Qnxn[inner_first]]]*second)' to an equivalent formula of the form 'Q'1x1[Q'2x2[Q'nxn[(inner_first*second)]]]' and proves the equivalence of these two formulas.

Parameters

formula (Formula) – formula with uniquely named variables to convert, whose root is a binary operator, i.e., which is of the form '(Q1x1[Q2x2[Qnxn[inner_first]]]*second)' where * is a binary operator, n>=0, each Qi is a quantifier, each xi is a variable name, and inner_first does not start with a quantifier.

Return type

Tuple[Formula, Proof]

Returns

A pair. The first element of the pair is a formula equivalent to the given formula, but of the form 'Q'1x1[Q'2x2[Q'nxn[(inner_first*second)]]]' where each Q'i is a quantifier, and where the operator *, the xi variable names, inner_first, and second are the same as in the given formula. The second element of the pair is a proof of the equivalence of the given formula and the returned formula (i.e., a proof of equivalence_of(formula,returned_formula)) via AXIOMS and ADDITIONAL_QUANTIFICATION_AXIOMS.

Examples

>>> formula = Formula.parse('(Ax[Ey[R(x,y)]]&Ez[P(1,z)])')
>>> returned_formula, proof = _pull_out_quantifications_from_left_across_binary_operator(
...     formula)
>>> returned_formula
Ax[Ey[(R(x,y)&Ez[P(1,z)])]]
>>> proof.is_valid()
True
>>> proof.conclusion == equivalence_of(formula, returned_formula)
True
>>> proof.assumptions == Prover.AXIOMS.union(
...     ADDITIONAL_QUANTIFICATION_AXIOMS)
True
predicates.prenex._pull_out_quantifications_from_right_across_binary_operator(formula)

Converts the given formula with uniquely named variables of the form '(first*Q1x1[Q2x2[Qnxn[inner_second]]])' to an equivalent formula of the form 'Q'1x1[Q'2x2[Q'nxn[(first*inner_second)]]]' and proves the equivalence of these two formulas.

Parameters

formula (Formula) – formula with uniquely named variables to convert, whose root is a binary operator, i.e., which is of the form '(first*Q1x1[Q2x2[Qnxn[inner_second]]])' where * is a binary operator, n>=0, each Qi is a quantifier, each xi is a variable name, and inner_second does not start with a quantifier.

Return type

Tuple[Formula, Proof]

Returns

A pair. The first element of the pair is a formula equivalent to the given formula, but of the form 'Q'1x1[Q'2x2[Q'nxn[(first*inner_second)]]]' where each Q'i is a quantifier, and where the operator *, the xi variable names, first, and inner_second are the same as in the given formula. The second element of the pair is a proof of the equivalence of the given formula and the returned formula (i.e., a proof of equivalence_of(formula,returned_formula)) via AXIOMS and ADDITIONAL_QUANTIFICATION_AXIOMS.

Examples

>>> formula = Formula.parse('(Ax[Ey[R(x,y)]]|Ez[P(1,z)])')
>>> returned_formula, proof = _pull_out_quantifications_from_right_across_binary_operator(
...     formula)
>>> returned_formula
Ez[(Ax[Ey[R(x,y)]]|P(1,z))]
>>> proof.is_valid()
True
>>> proof.conclusion == equivalence_of(formula, returned_formula)
True
>>> proof.assumptions == Prover.AXIOMS.union(
...     ADDITIONAL_QUANTIFICATION_AXIOMS)
True
predicates.prenex._pull_out_quantifications_across_binary_operator(formula)

Converts the given formula with uniquely named variables of the form '(Q1x1[Q2x2[Qnxn[inner_first]]]*P1y1[P2y2[Pmym[inner_second]]])' to an equivalent formula of the form 'Q'1x1[Q'2x2[Q'nxn[P'1y1[P'2y2[P'mym[(inner_first*inner_second)]]]]]]' and proves the equivalence of these two formulas.

Parameters

formula (Formula) – formula with uniquely named variables to convert, whose root is a binary operator, i.e., which is of the form '(Q1x1[Q2x2[Qnxn[inner_first]]]*P1y1[P2y2[Pmym[inner_second]]])' where * is a binary operator, n>=0, m>=0, each Qi and Pi is a quantifier, each xi and yi is a variable name, and neither inner_first nor inner_second starts with a quantifier.

Return type

Tuple[Formula, Proof]

Returns

A pair. The first element of the pair is a formula equivalent to the given formula, but of the form 'Q'1x1[Q'2x2[Q'nxn[P'1y1[P'2y2[P'mym[(inner_first*inner_second)]]]]]]' where each Q'i and P'i is a quantifier, and where the operator *, the xi and yi variable names, inner_first, and inner_second are the same as in the given formula. The second element of the pair is a proof of the equivalence of the given formula and the returned formula (i.e., a proof of equivalence_of(formula,returned_formula)) via AXIOMS and ADDITIONAL_QUANTIFICATION_AXIOMS.

Examples

>>> formula = Formula.parse('(Ax[Ey[R(x,y)]]->Ez[P(1,z)])')
>>> returned_formula, proof = _pull_out_quantifications_across_binary_operator(
...     formula)
>>> returned_formula
Ex[Ay[Ez[(R(x,y)->P(1,z))]]]
>>> proof.is_valid()
True
>>> proof.conclusion == equivalence_of(formula, returned_formula)
True
>>> proof.assumptions == Prover.AXIOMS.union(
...     ADDITIONAL_QUANTIFICATION_AXIOMS)
True
predicates.prenex._to_prenex_normal_form_from_uniquely_named_variables(formula)

Converts the given formula with uniquely named variables to an equivalent formula in prenex normal form, and proves the equivalence of these two formulas.

Parameters

formula (Formula) – formula with uniquely named variables to convert.

Return type

Tuple[Formula, Proof]

Returns

A pair. The first element of the pair is a formula equivalent to the given formula, but in prenex normal form. The second element of the pair is a proof of the equivalence of the given formula and the returned formula (i.e., a proof of equivalence_of(formula,returned_formula)) via AXIOMS and ADDITIONAL_QUANTIFICATION_AXIOMS.

Examples

>>> formula = Formula.parse('(~(Ax[Ey[R(x,y)]]->Ez[P(1,z)])|S(w))')
>>> returned_formula, proof = _to_prenex_normal_form_from_uniquely_named_variables(
...     formula)
>>> returned_formula
Ax[Ey[Az[(~(R(x,y)->P(1,z))|S(w))]]]
>>> proof.is_valid()
True
>>> proof.conclusion == equivalence_of(formula, returned_formula)
True
>>> proof.assumptions == Prover.AXIOMS.union(
...     ADDITIONAL_QUANTIFICATION_AXIOMS)
True
predicates.prenex.to_prenex_normal_form(formula)

Converts the given formula to an equivalent formula in prenex normal form, and proves the equivalence of these two formulas.

Parameters

formula (Formula) – formula to convert, which contains no variable names starting with z.

Return type

Tuple[Formula, Proof]

Returns

A pair. The first element of the pair is a formula equivalent to the given formula, but in prenex normal form. The second element of the pair is a proof of the equivalence of the given formula and the returned formula (i.e., a proof of equivalence_of(formula,returned_formula)) via AXIOMS and ADDITIONAL_QUANTIFICATION_AXIOMS.

Examples

>>> formula = Formula.parse('~(w=x|Aw[(Ex[(x=w&Aw[w=x])]->Ax[x=y])])')
>>> returned_formula, proof = to_prenex_normal_form(formula)
>>> returned_formula
Ez58[Ez17[Az4[Ez32[~(w=x|((z17=z58&z4=z17)->z32=y))]]]]
>>> proof.is_valid()
True
>>> proof.conclusion == equivalence_of(formula, returned_formula)
True
>>> proof.assumptions == Prover.AXIOMS.union(
...     ADDITIONAL_QUANTIFICATION_AXIOMS)
True