pylogic.proposition package

Subpackages

Submodules

pylogic.proposition.and_ module

class pylogic.proposition.and_.And(*propositions: Unpack[Ps], is_assumption: bool = False, description: str = '', **kwargs)[source]

Bases: _Junction[Unpack[Ps]]

all_proven() → Self[source]

Logical inference rule. If all propositions are proven, the conjunction is proven.

de_morgan() → Proposition[source]

Apply De Morgan’s law to the conjunction to get an equivalent proposition.

In intuitionistic logic, the only valid De Morgan’s laws are

~A and ~B <-> ~(A or B)

~A or ~B -> ~(A and B).

In this case, the conjunction must be made of negations to return a different result..

extract()[source]

Logical inference rule. Get all conjunct of a conjunction as a tuple.

Will prove all conjuncts if the conjunction is proven.

extract_conjuncts()[source]
remove_duplicates() → And[source]

Remove duplicate propositions from the _junction. Returns an equivalent proposition.

to_exor() → ExOr[Proposition, ...][source]

Logical inference rule. If self is of the form And(Or(A, B, C,…), A -> [~B /~C /...], B -> [~A /~C /...], C -> [~A /~B /...], …),

return ExOr(A, B, C, …).

This can be slow if there are many propositions in the Or.

Raises:

  • AssertionError – If wrong structure of propositions is given.

  • AttributeError – If the second, third, etc to the last proposition

  • are not all implications with conjunctions as consequents. –

to_sympy() → SpAnd[source]
class pylogic.proposition.and_.InferenceRule

Bases: dict

arguments: list[str]
name: str

pylogic.proposition.contradiction module

class pylogic.proposition.contradiction.Contradiction(**kwargs)[source]

Bases: 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

class pylogic.proposition.contradiction.InferenceRule

Bases: dict

arguments: list[str]
name: str

pylogic.proposition.exor module

class pylogic.proposition.exor.ExOr(*propositions: Unpack[Ps], is_assumption: bool = False, description: str = '', **kwargs)[source]

Bases: _Junction[Unpack[Ps]]

This proposition is proven when exactly one of the propositions is proven and the negations of the other propositions are proven. In other words, it is true when exactly one of the propositions is true and all the others are false. We may not know which proposition is true, but we know that only one is true.

classmethod one_proven(positive_proven: Proposition, *negations_proven: Proposition) → Self[source]

Logical inference rule. Given that one proposition is proven and all the negations of the other propositions are proven, return a proof of an ExOr.

one_proven_rem_false(p: Proposition) → And[*Props,][source]

Logical inference rule. Given self is proven, and one proven proposition in self, return a proof that all the remaining propositions are false.

remove_duplicates() → ExOr[source]

Remove duplicate propositions from the _junction. Returns an equivalent proposition.

pylogic.proposition.exor.Exor

alias of ExOr

class pylogic.proposition.exor.InferenceRule

Bases: dict

arguments: list[str]
name: str

pylogic.proposition.iff module

class pylogic.proposition.iff.Iff(left: TProposition, right: UProposition, is_assumption: bool = False, description: str = '', **kwargs)[source]

Bases: Proposition, Generic[TProposition, UProposition]

as_text(*, _indent=0) → str[source]

Return a text representation of the proposition.

contrapositive() → Iff[Not[UProposition], Not[TProposition]][source]

Logical inference rule. Given self (A <-> B) is proven, return the contrapositive ~B <-> ~A.

converse() → Iff[UProposition, TProposition][source]

Logical inference rule. Given self (A <-> B) is proven, return the converse B <-> A.

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

describe(*, _indent=0) → str[source]

Return a description of the proposition.

forward_implication() → Implies[TProposition, UProposition][source]

Logical inference rule. Given self (A <-> B) is proven, return the forward implication A -> B.

has_as_subproposition(other: Proposition) → bool[source]

Check if other is a subproposition of self.

inverse() → Iff[Not[TProposition], Not[UProposition]][source]

Logical inference rule. Given self (A <-> B) is proven, return the inverse ~A <-> ~B.

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.

reverse_implication() → Implies[UProposition, TProposition][source]

Logical inference rule. Given self (A <-> B) is proven, return the reverse implication B -> A.

to_conjunction() → And[Implies[TProposition, UProposition], Implies[UProposition, TProposition]][source]

If self is of the form A <-> B, returns a proposition of the form A -> B and B -> A

to_sympy() → Equivalent[source]
class pylogic.proposition.iff.InferenceRule

Bases: dict

arguments: list[str]
name: str

pylogic.proposition.implies module

class pylogic.proposition.implies.Implies(antecedent: TProposition, consequent: UProposition, is_assumption: bool = False, description: str = '', **kwargs)[source]

Bases: Proposition, Generic[TProposition, UProposition]

as_text(*, _indent=0) → str[source]

Return a text representation of the proposition.

contrapositive() → Implies[Proposition, Proposition][source]

Logical inference rule. Given self (A -> B) is proven, return the corresponding contrapositive (~B -> ~A)

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

definite_clause_resolve(in_body: list[Proposition] | tuple[Proposition, ...] | And[Proposition, ...], **kwargs) → Self | Implies[Proposition, UProposition] | UProposition[source]

Logical inference rule. Given self (A /B /C…) -> D is proven, and given a conjunction (or list representing a conjunction) of some props in the antecedent (say A and B) is proven, return a proof of the new definite clause (C /…) -> D or C -> D if only C is left in the body, or D if the antecedent is left empty.

describe(*, _indent=0) → str[source]

Return a description of the proposition.

first_unit_definite_clause_resolve(first_in_body: Proposition, **kwargs) → Self | Implies[Proposition, UProposition] | UProposition[source]

Logical inference rule. Given self (A /B /C…) -> D is proven, given A is proven, return a proof of the new definite clause (B /C /…) -> D or D if the antecedent is left empty. Slightly faster than unit_definite_clause_resolve.

has_as_subproposition(other: Proposition) → bool[source]

Check if other is a subproposition of self.

hypothetical_syllogism(*others: Implies) → Implies[source]

Logical inference rule. If self is A->B, and others are B->C, C->D, …, Y->Z, return A->Z.

The antecedent of the next proposition must be the consequent of the previous one.

impl_elim() → Or[source]

Logical inference rule. Given self (A -> B) is proven, return the corresponding disjunction form (~A / B).

This only works in classical logic, and will raise an error otherwise. Set pylogic.enviroment_settings.settings.settings[“USE_CLASSICAL_LOGIC”] = True to use this.

replace(replace_dict: dict[Any, Any], positions: list[list[int]] | None = None, equal_check: Callable[[Any, Any], bool] | None = None) → Implies[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_sympy() → SpImplies[source]
unify(other: Self) → Any | Literal[True] | None[source]

Algorithm to unify two propositions. If unification succeeds, a dictionary of values to instantiate variables to is returned. The dictionary never instantiates a variable y to variable y. It may instantiate a variable y to variable x or a variable y to a symbol or value y. If no instantiations need to be made (eg propositions are equal), return True. Otherwise (unification fails), return None.

Will also unify pylogic.Expr (unevaluated expressions).

unit_definite_clause_resolve(in_body: Proposition, **kwargs) → Self | Implies[Proposition, UProposition] | UProposition[source]

Logical inference rule. Given self (A /B /C…) -> D is proven, and given one of the props (say B) in the antecedent is proven, return a proof of the new definite clause (A /C /…) -> D or A -> D if only A is left in the body, or D if the antecedent is left empty.

class pylogic.proposition.implies.InferenceRule

Bases: dict

arguments: list[str]
name: str

pylogic.proposition.not_ module

class pylogic.proposition.not_.InferenceRule

Bases: dict

arguments: list[str]
name: str
class pylogic.proposition.not_.Not(negated: TProposition, is_assumption: bool = False, description: str = '', **kwargs)[source]

Bases: Proposition, Generic[TProposition]

as_text(*, _indent=0) → str[source]

Return a text representation of the proposition.

by_inspection_check() → bool | None[source]

Check if self is provable by inspection. Returns True if self.negated.by_inspection() returns False, False if self.negated.by_inspection() returns True, 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

de_morgan() → Proposition[source]

Apply De Morgan’s law to this negation.

In intuitionistic logic, the only valid De Morgan’s laws are

~A and ~B <-> ~(A or B)

~A or ~B -> ~(A and B).

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

describe(*, _indent=0) → str[source]

Return a description of the proposition.

has_as_subproposition(other: Proposition) → bool[source]

Check if other is a subproposition of self.

modus_tollens(other: Implies[Not[UProposition], TProposition]) → UProposition[source]
modus_tollens(other: Implies[UProposition, TProposition]) → Not[UProposition]

Logical inference rule. other: Implies

Must be an implication that has been proven whose structure is OtherProposition -> ~self

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.

symmetric() → Not[BinaryRelation][source]

Logical inference rule. If self is ~(a R b), where R is a symmetric relation, return a proof of ~(b R a).

to_sympy() → SpNot[source]
unify(other: Self) → Any | Literal[True] | None[source]

Algorithm to unify two propositions. If unification succeeds, a dictionary of values to instantiate variables to is returned. The dictionary never instantiates a variable y to variable y. It may instantiate a variable y to variable x or a variable y to a symbol or value y. If no instantiations need to be made (eg propositions are equal), return True. Otherwise (unification fails), return None.

Will also unify pylogic.Expr (unevaluated expressions).

pylogic.proposition.not_.are_negs(p: Proposition, q: Proposition) → bool[source]

Given two propositions, determine if they are negations of each other.

pylogic.proposition.not_.neg(p: Not[TProposition], is_assumption: bool = False, **kwargs) → TProposition[source]
pylogic.proposition.not_.neg(p: TProposition, is_assumption: bool = False, **kwargs) → Not[TProposition]

Given a proposition, return its negation. In intuitionistic logic, double-negation-elimination is not valid, so the result of neg(Not(p)) is ~~p.

In classical logic, double-negation-elimination is valid, so the result of neg(Not(p)) is p. Keyword arguments are not used in this case for neg(Not(p)): the result is p.

pylogic.proposition.not_.not_(p: Not[TProposition] | TProposition, is_assumption: bool = False, **kwargs) → Not[TProposition] | TProposition

Given a proposition, return its negation. In intuitionistic logic, double-negation-elimination is not valid, so the result of neg(Not(p)) is ~~p.

In classical logic, double-negation-elimination is valid, so the result of neg(Not(p)) is p. Keyword arguments are not used in this case for neg(Not(p)): the result is p.

pylogic.proposition.or_ module

class pylogic.proposition.or_.InferenceRule

Bases: dict

arguments: list[str]
name: str
class pylogic.proposition.or_.Or(*propositions: Unpack[Ps], is_assumption: bool = False, description: str = '', **kwargs)[source]

Bases: _Junction[Unpack[Ps]]

de_morgan() → Proposition[source]

Logical inference rule. Apply De Morgan’s law to the disjunction to get an equivalent proposition.

In intuitionistic logic, the only valid De Morgan’s laws are

~A and ~B <-> ~(A or B)

~A or ~B -> ~(A and B).

one_proven(p: Proposition) → Self[source]

Logical inference rule. Given one proven proposition in self, return a proof of self (disjunction).

remove_duplicates() → Or[source]

Remove duplicate propositions from the _junction. Returns an equivalent proposition.

to_sympy() → SpOr[source]

pylogic.proposition.proposition module

class pylogic.proposition.proposition.InferenceRule

Bases: dict

arguments: list[str]
name: str
class pylogic.proposition.proposition.Proposition(name: str, is_assumption: bool = False, is_axiom: bool = False, description: str = '', args: list[Term] | None = None, **kwargs)

Bases: object

Create a Proposition. A proposition is a declarative logical statement.

Parameters:

  • name (str) – Name of the proposition.

  • is_assumption (bool) – Whether this proposition is an assumption. Assumptions are true only within the context they are made.

  • is_axiom (bool) – Whether this proposition is an axiom. Axioms are true in all contexts.

  • description (str) – A description of what this proposition is.

  • args (list[Term] | None) – The arguments of the proposition. If None, the proposition has no arguments.

name

Name of the proposition.

Type:

str

is_assumption

Whether this proposition is an assumption. Assumptions are true only within the context they are made.

Type:

bool

is_axiom

Whether this proposition is an axiom. Axioms are true in all contexts.

Type:

bool

description

A description of this proposition.

Type:

str

args

The arguments of the proposition.

Type:

list[Term] | None

arity

The number of arguments of the proposition.

Type:

int

is_proven

Whether the proposition has been proven. If is_proven is False, the proposition is not necessarily false, but it is not proven to be true.

Type:

bool

from_assumptions

The assumptions that were used to deduce this proposition.

Type:

set[Proposition]

deduced_from

The inference that was used to deduce this proposition. This will not be None if the proposition was proven using inference rules. This is None if is_proven is False, or if is_axiom is True while is_asumption is False.

Type:

Inference | None

Example

>>> p = Proposition("p", args=[1, 2])
>>> p.name
'p'
>>> p.args
[Constant(1, deps=()), Constant(2, deps=())]
>>> p.is_assumption
False
and_(*others: *Props, is_assumption: bool = False, allow_duplicates: bool = False, **kwargs) → And[Self, *Props] | And

Logical inference rule.

Combine this proposition with others using a conjunction. Continguous And objects are combined into one And sequence to reduce nesting. allow_duplicates: bool

If True, we do not remove duplicate propositions.

If all propositions are proven, the resulting proposition is proven.

Examples

>>> p1 = x.is_in(A)
>>> p2 = y.is_in(B)
>>> p3 = p1.and_(p2)
>>> p3
x in A /\ y in B
and_reverse(*others: *Props, is_assumption: bool = False, allow_duplicates: bool = False, **kwargs) → And[*Props, Self] | And

Combine this proposition with others using a conjunction, with self at the end. Continguous And objects are combined into one And sequence to reduce nesting. allow_duplicates: bool

If True, we do not remove duplicate propositions.

as_text(*, _indent=0) → str

Return a text representation of the proposition. Subpropositions are indented further right. One indentation is 2 spaces.

Returns:

A text representation of the proposition.

Return type:

str

assume(**kwargs) → Self

Logical inference rule.

Mark the proposition as an assumption.

Returns:

The proposition itself.

Return type:

Self

property atoms: set[Symbol | Set]

All the atomic symbols and sets in the proposition. This includes variables, constants, sets and classes.

by_inspection() → Self

Logical inference rule. Try to prove the proposition by inspection.

by_inspection_check() → bool | None

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.

close_all_scopes() → Proposition

Close all scopes in the proposition. If assumptions (A) were used to deduce this proposition (self), they are removed and we get a proof of A -> self. If variables exist in the proposition, they are universally quantified. Universal quantifiers scopes are closed last so they are outermost.

contradicts(other: Proposition) → Contradiction

Logical inference rule. If self and other are negations (and both proven), return a contradiction.

Examples

>>> p1 = prop("P").assume()
>>> p2 = neg(prop("P")).assume()
>>> p3 = p1.contradicts(p2)
>>> p3, p3.is_proven
(contradiction, True)
copy() → Self

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

de_morgan() → Self

Apply De Morgan’s law to self to return an equivalent proposition.

In intuitionistic logic, the only valid De Morgan’s laws are

~A and ~B <-> ~(A or B)

~A or ~B -> ~(A and B).

deepcopy() → Self

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: Proposition

A(n expanded) definition of the proposition.

describe(*, _indent=0) → str

Return a description of the proposition. If no description is set, it calls as_text() to get a text representation of the proposition.

Returns:

A description of the proposition.

Return type:

str

eval_same(other: Proposition) → bool

Check if two propositions evaluate to equal propositions. We check if the names are equal and if all the corresponding arguments evaluate to equal terms.

Parameters:

other (Proposition) – The proposition to compare to.

Returns:

True if the propositions are evaluate to the same proposition, False otherwise.

Return type:

bool

Examples

>>> p1 = Proposition("p", args=[2])
>>> p2 = Proposition("p", args=[Add(1, 1)])
>>> p1.eval_same(p2)
True
followed_from(*assumptions, **kwargs)

Given self is proven, return a new proposition that is an implication of the form And(*assumptions) -> self. *assumptions: Proposition

Propositions that implied this proposition.

This function only accepts propositions that were explicitly declared as assumptions and used to deduce self.

Note that after this function is called, the assumptions are no longer considered assumptions. You would need to assume them again if you want to use them in another deduction.

has_as_subproposition(other: Proposition) → bool

Check if other is a subproposition of self.

iff(other: TProposition, is_assumption: bool = False, **kwargs) → Iff[Self, TProposition]

Create a biconditional between this proposition and another.

implies(other: TProposition | Implies[TProposition, UProposition], is_assumption: bool = False, de_nest: bool = True, **kwargs) → Implies[Self, TProposition] | Implies[And[Self, TProposition], UProposition]

Create an implication from this proposition to another. If other is an implication A -> B and de_nest = True, we return an implication (self /A) -> B.

classmethod inference_rules() → list[str]

Return a list of inference rules that are implemented in this class.

Returns:

A list of inference rules that are implemented in this class.

Return type:

list[str]

is_one_of(other: And, *, _Proposition__recursing: bool = False) → Self

Logical inference rule. If we have proven other, we can prove any of the propositions in it. other: And

Must be a conjunction that has been proven where one of the propositions is self.

Examples

>>> p1 = prop("P")
>>> p2 = prop("Q")
>>> p3 = prop("R")
>>> p4 = And(p1, p2, p3).assume()
>>> p5 = p1.is_one_of(p4)
>>> p5, p5.is_proven
(P, True)
property is_proven: bool

Whether the proposition has been proven. If is_proven is False, the proposition is not necessarily false, but it is not proven to be true.

is_special_case_of(other: Forall[Self]) → Self

Logical inference rule. other: Proposition

A proven forall proposition that implies this proposition.

Examples

>>> p1 = prop("P", 1)
>>> p2_proven = Forall(x, prop("P", x)).assume()
>>> p1_proven = p1.is_special_case_of(p2_proven)
>>> p1_proven.is_proven
True
modus_ponens(other: Implies[Self, TProposition] | Iff[Self, TProposition], **kwargs) → TProposition

Logical inference rule. other: Implies

Must be an implication that has been proven whose structure is self -> OtherProposition

Examples

>>> p1 = prop("P").assume() # P
>>> p2 = prop("P").implies(prop("Q")).assume() # P -> Q
>>> p3 = p1.modus_ponens(p2) # infer Q
>>> p3, p3.is_proven
(Q, True)
modus_tollens(other: Implies[Not[TProposition], Not[Self]] | Implies[TProposition, Not[Self]] | Iff) → TProposition | Not[TProposition]

Logical inference rule. other: Implies

Must be an implication that has been proven whose structure is OtherProposition -> ~self

Examples

>>> p1 = neg(prop("P")).assume() # ~P
>>> p2 = prop("Q").implies(prop("P")).assume() # Q -> P
>>> p3 = p1.modus_tollens(p2) # infer ~Q
>>> p3, p3.is_proven
(~Q, True)
mp(other: Implies[Self, TProposition] | Iff[Self, TProposition], **kwargs) → TProposition

Logical inference rule. other: Implies

Must be an implication that has been proven whose structure is self -> OtherProposition

Examples

>>> p1 = prop("P").assume() # P
>>> p2 = prop("P").implies(prop("Q")).assume() # P -> Q
>>> p3 = p1.modus_ponens(p2) # infer Q
>>> p3, p3.is_proven
(Q, True)
mt(other: Implies[Not[TProposition], Not[Self]] | Implies[TProposition, Not[Self]] | Iff) → TProposition | Not[TProposition]

Logical inference rule. other: Implies

Must be an implication that has been proven whose structure is OtherProposition -> ~self

Examples

>>> p1 = neg(prop("P")).assume() # ~P
>>> p2 = prop("Q").implies(prop("P")).assume() # Q -> P
>>> p3 = p1.modus_tollens(p2) # infer ~Q
>>> p3, p3.is_proven
(~Q, True)
or_(*others: *Props, is_assumption: bool = False, allow_duplicates: bool = False, **kwargs) → Or[Self, *Props] | Or

Logical inference rule.

Combine this proposition with others using a disjunnction. Continguous Or objects are combined into one Or sequence to reduce nesting. allow_duplicates: bool

If True, we do not remove duplicate propositions.

If any proposition is proven, the resulting proposition is proven.

Examples

>>> p1 = x.is_in(A)
>>> p2 = y.is_in(B)
>>> p3 = p1.or_(p2)
>>> p3
x in A \/ y in B
or_reverse(*others: *Props, is_assumption: bool = False, allow_duplicates: bool = False, **kwargs) → Or[*Props, Self] | Or

Combine this proposition with others using a disjunction, with self at the end. Continguous Or objects are combined into one Or sequence to reduce nesting. allow_duplicates: bool

If True, we do not remove duplicate propositions.

p_and(*others: *Props, allow_duplicates: bool = False) → And[Self, *Props]

Same as and_, but returns a proven proposition when self and all others are proven.

p_and_reverse(*others: *Props, allow_duplicates: bool = False) → And[*Props, Self]

Logical inference rule. Same as and_reverse, but returns a proven proposition when self and all others are proven.

p_substitute(side: Side | str, equality: Equals) → Self
Parameters:

  • side (Side) – Side.LEFT or Side.RIGHT

  • equality (Equals) – An equality proposition. We look for the other side of the equality in self and replace it with the ‘side’.

  • proposition. (Returns a proven)

replace(replace_dict: dict[Term, Term], positions: list[list[int]] | None = None, equal_check: Callable[[Term, Term], bool] | None = None) → Proposition

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.

set_desc(description: str) → Self

Set the description of the proposition.

Parameters:

description (str) – The description of the proposition.

Returns:

The proposition itself.

Return type:

Self

set_description(description: str) → Self

Set the description of the proposition.

Parameters:

description (str) – The description of the proposition.

Returns:

The proposition itself.

Return type:

Self

substitute(side: Side | str, equality: Equals, **kwargs) → Self

Logical inference rule.

If self is proven and equality is proven, we can substitute the side of the equality into self.

Parameters:

  • side (Side) – Side.LEFT or Side.RIGHT The side of the equality to appear in the result

  • equality (Equals) – An equality proposition. We look for the other side of the equality in self and replace it with the ‘side’.

property symbols: set[Symbol]

All the symbols in the proposition. This includes variables and constants.

thus_forall(variable_or_containment: Variable | IsContainedIn[Term, Set | Variable | Class], set_: Set | Variable | Class | None = None, **kwargs) → Forall[Self] | ForallInSet[Self]

Given self is proven, return a new proposition that for all variables, self is true. This inference rule binds the variable, so you cannot reuse the variable unless you unbind it.

thus_there_exists(existential_var: str, expression_to_replace: Term, set_: Set | Variable | Class | None = None, expression_to_replace_is_in_set: IsContainedIn[Term, Set | Variable | Class] | None = None, latex_name: str | None = None, positions: list[list[int]] | None = None) → Exists[Self]

Logical inference rule. Given self is proven, return a new proposition that there exists an existential_var such that self is true, when self is expressed in terms of that existential_var. For example, if self is x^2 + x > 0, existential_var is y and expression_to_replace is x^2, then we return the proven proposition Exists y: y + x > 0.

existential_var: str

A new variable that is introduced into our new existential proposition.

expression_to_replace: Set | SympyExpression

An expression that is replaced by the new variable.

set_: Set

The set in which the existential variable is contained.

expression_to_replace_is_in_set: IsContainedIn

A proposition that states that the expression_to_replace is in the set_.

latex_name: str | None

The latex representation of the existential variable.

positions: list[list[int]]

This is a list containing the positions of the expression_to_replace in self. If None, we will search for all occurences of the expression_to_replace in self. This is a nested list representing the path we need to go down in the proposition tree, For example, if self is (forall x: (p1 x -> p2 x) /(p3 x) /(p4 x)) -> (p5 x) existential_var = q 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)

Examples

>>> p1 = prop("P", 1).assume() # P(1)
>>> p2 = p1.thus_there_exists("x", 1)
>>> p2, p2.is_proven
(exists x: P(x), True)
todo(**kwargs) → Self

Mark the proposition as proven, but not yet implemented.

Returns:

The proposition itself.

Return type:

Self

Warns:

UserWarning – Lets the user know that this proposition is not actually proven yet.

unify(other: Proposition) → Unification | Literal[True] | None

Algorithm to unify two propositions. If unification succeeds, a dictionary of values to instantiate variables to is returned. The dictionary never instantiates a variable y to variable y. It may instantiate a variable y to variable x or a variable y to a symbol or value y. If no instantiations need to be made (eg propositions are equal), return True. Otherwise (unification fails), return None.

Will also unify pylogic.Expr (unevaluated expressions).

xor(*others: *Props, is_assumption: bool = False, allow_duplicates: bool = False, **kwargs) → ExOr[Self, *Props] | ExOr

Combine this proposition with others using an exclusive or. Continguous ExOr objects are combined into one ExOr sequence to reduce nesting. allow_duplicates: bool

If True, we do not remove duplicate propositions.

Examples

>>> p1 = x.is_in(A)
>>> p2 = y.is_in(B)
>>> p3 = p1.xor(p2)
>>> p3
x in A xor y in B
xor_reverse(*others: *Props, is_assumption: bool = False, allow_duplicates: bool = False, **kwargs) → ExOr[*Props, Self] | ExOr

Combine this proposition with others using an exclusive or, with self at the end. Continguous ExOr objects are combined into one ExOr sequence to reduce nesting. allow_duplicates: bool

If True, we do not remove duplicate propositions.

pylogic.proposition.proposition.get_assumptions(p: Proposition) → set[Proposition]

Given a proposition, return the assumptions that were used to deduce it.

pylogic.proposition.proposition.pred(name: str) → Callable[[...], Proposition]

Create a predicate with a given name.

A predicate is a python function that returns a proposition.

When called, the function returns a proposition with the given name and arguments.

pylogic.proposition.proposition.predicate(name: str) → Callable[[...], Proposition]

Create a predicate with a given name.

A predicate is a python function that returns a proposition.

When called, the function returns a proposition with the given name and arguments.

pylogic.proposition.proposition.predicates(*names: str) → Callable[[...], Proposition] | tuple[Callable[[...], Proposition], ...]

Create multiple predicates with the given names.

pylogic.proposition.proposition.preds(*names: str) → Callable[[...], Proposition] | tuple[Callable[[...], Proposition], ...]

Create multiple predicates with the given names.

pylogic.proposition.proposition.prop(name: str, *args: Term, **kwargs) → Proposition

Create a proposition with a given name and arguments.

pylogic.proposition.proposition.proposition(name: str, *args: Term, **kwargs) → Proposition

Create a proposition with a given name and arguments.

pylogic.proposition.proposition.propositions(*names: str, args: tuple[Term, ...] = (), **kwargs) → Proposition | tuple[Proposition, ...]

Create multiple propositions with the given names.

pylogic.proposition.proposition.props(*names: str, args: tuple[Term, ...] = (), **kwargs) → Proposition | tuple[Proposition, ...]

Create multiple propositions with the given names.

Module contents