pylogic.theories package

Submodules

pylogic.theories.integers module

class pylogic.theories.integers.IntegersRing[source]
class pylogic.theories.integers.IntegersRing(*args, **kwargs)

Bases: RIng[Any], OrderedSet

divides(a: Z, b: Z, **kwargs) → Divides[source]
even(n: Term, **kwargs) → ExistsInSet[Equals][source]
odd(n: Term, **kwargs) → ExistsInSet[Equals][source]
predecessor: Function
successor: Function

pylogic.theories.natural_numbers module

class pylogic.theories.natural_numbers.NaturalsSemiring[source]
class pylogic.theories.natural_numbers.NaturalsSemiring(*args, **kwargs)

Bases: SemirIng, OrderedSet

closed_under_successor: ForallInSet[IsContainedIn]
divides(a: Term, b: Term, **kwargs) → Divides[source]
even(n: Any, **kwargs) → ExistsInSet[Equals][source]
odd(n: Any, **kwargs) → ExistsInSet[Equals][source]
prime(n: Any, **kwargs) → Prime[source]
classmethod property_closed_under_successor(set_: Set, successor: Function, **kwargs) → ForallInSet[IsContainedIn][source]
classmethod property_strong_induction_formal(set_: Set, total_order: TotalOrderOp, successor: Function, zero: Constant, **kwargs) → ForallSubsets[Implies[And[IsContainedIn, ForallInSet[Implies[ForallInSet[Implies[TotalOrder, IsContainedIn]], IsContainedIn]]], Equals]][source]

This uses second order logic (quantifying over subsets of N) to state the principle of strong induction. This is formal in the sense that it uses the successor function without evaluating it.

classmethod property_successor_injective(set_: Set, successor: Function, **kwargs) → ForallInSet[ForallInSet[Implies[Equals, Equals]]][source]
classmethod property_successor_neq_0(set_: Set, successor: Function, zero: Constant, **kwargs) → ForallInSet[Not[Equals]][source]
classmethod property_well_ordering_set(set_: Set, total_order: TotalOrderOp, **kwargs) → ForallSubsets[Implies[Not[Equals], ExistsInSet[ForallInSet[TotalOrder]]]][source]
classmethod property_zero_is_min_nat(set_: Set, total_order: TotalOrderOp, zero: Constant, **kwargs) → ForallInSet[TotalOrder][source]
strong_induction(base_case: Proposition, induction_step: ForallInSet[Implies[ForallInSet[Implies[TotalOrder, Proposition]], Proposition]]) → ForallInSet[Proposition][source]

Logical inference rule. This uses the principle of strong induction given the base case and inductive step. Given base case P(0) and induction step forall n in N:

forall k in N: (k <= n -> P(k)) implies P(n+1),

return a proof of forall n: n in N -> P(n).

strong_induction_formal: ForallSubsets[Implies[And[IsContainedIn, ForallInSet[Implies[ForallInSet[Implies[TotalOrder, IsContainedIn]], IsContainedIn]]], Equals]]
successor: Function
successor_injective

alias of ForallInSet[ForallInSet[Implies[Equals, Equals]]]

successor_neq_0: ForallInSet[Not[Equals]]
weak_induction(base_case: Proposition, induction_step: ForallInSet[Implies[Proposition, Proposition]]) → ForallInSet[Proposition][source]

Logical inference rule. This uses the principle of weak induction given the base case and inductive step. Given base case P(0) and induction step forall n in N: P(n) -> P(n+1), return a proof of forall n in N, P(n).

well_ordering(prop: Proposition, argument: Term | None = None) → ExistsInSet[And[Proposition, ForallInSet[Implies[Proposition, TotalOrder]]]][source]

Logical inference rule. Given a proposition about naturals, prove that there is a least natural number satisfying it. If argument is provided, it should be an argument of the proposition and will be used in patter-matching to construct the result.

well_ordering_set: ForallSubsets[Implies[Not[Equals], ExistsInSet[ForallInSet[TotalOrder]]]]
zero_is_min_nat: ForallInSet[TotalOrder]
class pylogic.theories.natural_numbers.Prime(n: Any, description: str = '', **kwargs)[source]

Bases: Proposition

Represents a number being prime.

by_inspection_check() → bool | None[source]

Check if self is provable by inspection. Returns True if self is provable by inspection, False if its negation is provable by inspection, and None if neither is provable.

copy() → Self[source]

Create a shallow copy of the proposition. The copy keeps the same references to the arguments, assumptions, and inference as the original proposition.

Returns:

A shallow copy of the proposition.

Return type:

Self

deepcopy() → Self[source]

Create a deep copy of the proposition. The copy creates new copies of the arguments of the proposition. The copy keeps the same references to the assumptions and inference as the original proposition.

Returns:

A deep copy of the proposition.

Return type:

Self

property definition: And

A(n expanded) definition of the proposition.

replace(replace_dict: dict[Any, Any], positions: list[list[int]] | None = None, equal_check: Callable[[Any, Any], bool] | None = None) → Self[source]

This function currently replaces Terms in the proposition with other Terms. It does not replace Propositions.

For each key in replace_dict, we replace it in the proposition with the corresponding new value.

positions is a list of lists of integers representing the occurences of the old values in the proposition. Each list of integers represents a path to the value in the proposition tree. Each integer in the list represents the index of the subproposition (or subexpression) in the list of subpropositions/arguments of the parent proposition.

Parameters:

  • replace_dict (dict[Term, Term]) – A dictionary where the keys are the Terms to be replaced and the values are the new Terms.

  • positions (list[list[int]] | None) –

    This is a list containing the positions of the old values in this instance. If None, we will replace for all occurences of the old values with the new values. The nested list represents the path we need to go down in the proposition tree.

    TODO: finish replace, document replacing the quantified variables as well

    For example, if self is (forall x: (p1 x -> p2 x) /(p3 x) /(p4 x)) -> (p5 x) current_val = x new_val = p and positions = [[0, 0, 0], [0, 2], [1]] we end up with exists q: (forall x: (p1 q -> p2 x) /(p3 x) /(p4 q)) -> (p5 q) The quantified variable in a forall is never replaced itself. Due to this, the positions array for forall goes directly into the inner proposition. Same for exists. In the example above, the first list [0,0,0] refers to the x in p1 x, not (p1 x -> p2 x).

  • equal_check (Callable[[Term, Term], bool] | None) – A function that takes two arguments and returns True if they compare equal. By default, it uses the == operator.

Returns:

A new proposition with the replaced values.

Return type:

Proposition

Examples

>>> x, y, a = variables("x", "y", "a")
>>> p1, p2, p3,  p4, p5 = predicates("p1", "p2", "p3", "p4", "p5")
>>> prop1 = Forall(x, p1(x, y).implies(p2(y)).and_(p3(y), p4(y))).implies(p5(y))
>>> prop1.replace({y: a}, positions=[[0, 0, 0], [0, 2], [1]])
(forall x: ((p1(x, a) -> p2(y)) /\ p3(y) /\ p4(a))) -> p5(a)
>>> prop1.replace({x: a}, positions=[[0, 0, 0]])
(forall a: ((p1(a, y) -> p2(y)) /\ p3(y) /\ p4(y))) -> p5(y)

Note

In the example above, the first list [0,0,0] refers to the proposition p1(x, y), so in the first call to replace(), all occurences of y in p1(x, y) are replaced with a.

pylogic.theories.numbers module

pylogic.theories.numbers.add_positive_gt_parts(set_)[source]
pylogic.theories.numbers.gt_implies_neq(set_)[source]
pylogic.theories.numbers.lt_implies_neq(set_)[source]

pylogic.theories.rational_numbers module

class pylogic.theories.rational_numbers.RationalsField[source]
class pylogic.theories.rational_numbers.RationalsField(*args, **kwargs)

Bases: Field[Any], OrderedSet

pylogic.theories.real_numbers module

class pylogic.theories.real_numbers.Interval[source]
class pylogic.theories.real_numbers.Interval(*args, **kwargs)

Bases: Set

evaluate(**kwargs)[source]
class pylogic.theories.real_numbers.IntervalFunc[source]

Bases: object

Returns an interval with the given bounds.

You can create a closed interval by using the subscript operator, or calling the function with the bounds as arguments for more flexibility.

arguments are either:

left_symbol: ‘[’ or ‘(’ a: Term b: Term right_symbol: ‘]’ or ‘)’

Returns an interval with the given bounds.

or:

*terms: Term two terms representing the bounds.

Returns an open interval with the given bounds.

or:

terms: Tuple[Term, Term]

Returns an open interval with the given bounds.

or:

terms: list[Term]

A list of two terms. Returns a closed interval with the given bounds.

Examples: >>> interval(“[”, 1, 2, “]”) [1, 2] >>> interval(“[”, 1, 2, “)”) [1, 2) >>> interval(1, 2) (1, 2) >>> interval((1, 2)) (1, 2) >>> interval([1, 2]) [1, 2] >>> interval[1, 2] [1, 2]

class pylogic.theories.real_numbers.RealsField[source]
class pylogic.theories.real_numbers.RealsField(*args, **kwargs)

Bases: Field[Any], OrderedSet

bounded_above(s) → Any[source]
bounded_above_has_lub: ForallSubsets[Implies[And[Not[Equals], BoundedAbove], HasLUB]]
has_lub(s) → Any[source]
is_ub(ub, s) → Any[source]
classmethod property_bounded_above_has_lub(set_: Set) → ForallSubsets[Implies[And[Not[Equals], Any], Any]][source]

Module contents