pylogic.proposition.relation package¶

Submodules¶

pylogic.proposition.relation.binaryrelation module¶

class pylogic.proposition.relation.binaryrelation.BinaryRelation(left: T, right: U, name: str = 'BR', is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: Relation, Generic[T, U]

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

infix_symbol: str = 'BR'¶

infix_symbol_latex: str = 'BR '¶

is_antisymmetric: bool = False¶

is_asymmetric: bool = False¶

is_connected: bool = False¶

is_irreflexive: bool = False¶

is_reflexive: bool = False¶

is_strongly_connected: bool = False¶

is_symmetric: bool = False¶

is_transitive: bool = False¶

name: str = 'BR'¶

classmethod reflexive(term: T) → C[source]¶: Logical inference rule. Given a term, return a reflexive relation of the form term R term.

replace(replace_dict: dict[Any, Any], positions: list[list[int]] | None = None, equal_check: Callable[[Any, Any], bool] | None = None) → Self[source]¶: Replace current_val with new_val in the relation.

symmetric() → BinaryRelation[U, T][source]¶: Logical inference rule. If self is proven, return a proof of self.right Relation self.left.

transitive(*others: Self) → Self[source]¶

Logical InferenceRule. If self is of the form a ~ b and other is of the form b ~ c, or of the form (b ~ c or b = c), returns a proven relation of the form a ~ c. Will try to evaluate expressions if self.right and other.left don’t have the same structure.

Raises NotImplementedError if the expression can’t be evaluated and it is needed.

pylogic.proposition.relation.contains module¶

class pylogic.proposition.relation.contains.InferenceRule¶

Bases: dict

arguments: list[str]¶

name: str¶

class pylogic.proposition.relation.contains.IsContainedIn(left: T, right: Any, is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: BinaryRelation[T, Any]

by_containment_func() → Self[source]¶: Logical inference rule. Use the set’s containment function to prove that it contains the element

by_definition() → Self[source]¶: Logical inference rule. Prove that the element is in the set by definition.

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.

by_predicate(proven_predicate: Proposition, **kwargs) → Self[source]¶: Logical inference rule. Use the set’s predicate function to prove that it contains the element

property element: T¶

infix_symbol: str = 'in'¶

infix_symbol_latex: str = '\\in'¶

is_transitive: bool = False¶

name: str = 'IsContainedIn'¶

thus_contained_in_all() → And[IsContainedIn, ...][source]¶: Logical inference rule. Given x in Intersection[A, B, C], return a proof that x in A and x in B and x in C

thus_contained_in_at_least_one() → Or[IsContainedIn, ...][source]¶: Logical inference rule. Given x in Union[A, B, C], return a proof that x in A or x in B or x in C

thus_contained_in_b(a_is_subset_b: IsSubsetOf) → IsContainedIn[source]¶: Logical inference rule. If self is proven and of the form x in A and A issubset B is given, returns a proven proposition of the form x in B

thus_not_empty() → Not[Equals][source]¶: Logical inference rule. Given self = x in S is proven, return a proof that S is not empty.

thus_predicate() → Proposition[source]¶: Logical inference rule. Given that the set contains the element, return the predicate that the element satisfies.

pylogic.proposition.relation.divides module¶

class pylogic.proposition.relation.divides.Divides(a: Any, b: Any, quotient_set: Any, is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: Relation

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: ExistsInSet¶: A(n expanded) definition of the proposition.

is_atomic = True¶

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.

to_exists_in_set(**kwargs) → ExistsInSet[source]¶

pylogic.proposition.relation.equals module¶

class pylogic.proposition.relation.equals.Equals(left: T, right: U, is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: BinaryRelation[T, U]

apply(f: Callable[[Any], Any]) → Equals[source]¶: Apply a function to both sides of the equality.

by_eval() → Self[source]¶: Return a proven equality if both sides evaluate to the same value.

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.

by_simplification() → Self[source]¶: Logical inference rule.

evaluate(**kwargs) → Equals[source]¶: Evaluate the equality.

get(side: Side | str) → Any[source]¶

infix_symbol: str = '='¶

infix_symbol_latex: str = '='¶

is_reflexive: bool = True¶

is_symmetric: bool = True¶

is_transitive: bool = True¶

name: str = 'Equals'¶

p_substitute_into(side: Side | str, other_prop: TProposition) → TProposition[source]¶: Logical inference rule. If side == Side.LEFT, will look for self.right in other_prop and replace it with self.left. Returns a proven proposition. :param side: Side to appear in the result. :type side: Side :param other_prop: Proposition to search for the other side in. :type other_prop: Proposition

substitute_into(side: Side | str, other_prop: TProposition, **kwargs) → TProposition[source]¶: If side == Side.LEFT, will look for self.right in other_prop and replace it with self.left. :param side: Side to appear in the result. :type side: Side :param other_prop: Proposition to search for the other side in. :type other_prop: Proposition

symmetric() → Equals[U, T][source]¶: Logical inference rule. If self is proven, return a proof of self.right Relation self.left.

to_sympy() → Equality[source]¶

zero_abs_is_0() → Equals[source]¶: Logical inference rule. If self is of the form Abs(x) = 0, return a proof of x = 0.

pylogic.proposition.relation.relation module¶

class pylogic.proposition.relation.relation.Relation(name: str, args: list[Any], is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: Proposition

as_text(*, _indent=0) → str[source]¶: Return a text representation of the proposition.

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

pylogic.proposition.relation.subsets module¶

class pylogic.proposition.relation.subsets.InferenceRule¶

Bases: dict

arguments: list[str]¶

name: str¶

class pylogic.proposition.relation.subsets.IsSubsetOf(left: Any, right: Any, is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: BinaryRelation[Any, Any]

by_empty() → Self[source]¶: Logical inference rule. If self is EmptySet issubset A, return self but proven

by_inspection() → Self[source]¶: Logical inference rule. If self is already proven, self is A issubset A, or the predicate of self.left logically implies that any variable x in self.left is in self.right, return self but proven.

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

infix_symbol: str = 'issubset'¶

infix_symbol_latex: str = '\\subseteq'¶

is_transitive: bool = True¶

name: str = 'IsSubsetOf'¶

to_forall() → Forall[Implies[IsContainedIn, IsContainedIn]][source]¶: If self is A issubset B, return forall x: x in A -> x in B

pylogic.proposition.relation package¶

Submodules¶

pylogic.proposition.relation.binaryrelation module¶

pylogic.proposition.relation.contains module¶

pylogic.proposition.relation.divides module¶

pylogic.proposition.relation.equals module¶

pylogic.proposition.relation.relation module¶

pylogic.proposition.relation.subsets module¶

Module contents¶

Pylogic

Navigation

Related Topics