pylogic.proposition.ordering package¶

Submodules¶

pylogic.proposition.ordering.greaterorequal module¶

class pylogic.proposition.ordering.greaterorequal.GreaterOrEqual(left: T, right: U, is_assumption: bool = False, description: str = '', name=None, **kwargs)[source]¶

Bases: TotalOrder[T, U], _Ordering

add_negative_to_right(negative: Any) → GreaterThan[source]¶: Logical inference rule. If self is of the form a >= b and c is negative, returns a proposition of the form a > b + c

add_nonnegative_to_left(nonnegative: Any) → GreaterOrEqual[source]¶: Logical inference rule. If self is of the form a >= b and c is nonnegative, returns a proposition of the form a + c >= b

add_nonpositive_to_right(nonpositive: Any) → GreaterOrEqual[source]¶: Logical inference rule. If self is of the form a >= b and c is nonpositive (c <= 0), returns a proposition of the form a >= b + c

add_positive_to_left(positive: Any) → GreaterThan[source]¶: Logical inference rule. If self is of the form a >= b and c is positive, returns a proposition of the form a + c > b

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.

infix_symbol: str = '>='¶

infix_symbol_latex: str = '\\geq'¶

name: str = 'GreaterOrEqual'¶

to_disjunction() → Or[GreaterThan, Equals][source]¶: If self is of the form a >= b, returns a proposition of the form a > b or a = b

pylogic.proposition.ordering.greaterthan module¶

class pylogic.proposition.ordering.greaterthan.GreaterThan(left: T, right: U, is_assumption: bool = False, description: str = '', name=None, **kwargs)[source]¶

Bases: StrictTotalOrder[T, U], _Ordering

add_nonnegative_to_left(nonnegative: Any) → GreaterThan[source]¶: Logical inference rule. If self is of the form a > b and c is nonnegative, returns a proposition of the form a + c > b

add_nonpositive_to_right(nonpositive: Any) → GreaterThan[source]¶: Logical inference rule. If self is of the form a > b and c is nonpositive (c <= 0), returns a proposition of the form a > b + c

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.

infix_symbol: str = '>'¶

infix_symbol_latex: str = '>'¶

mul_inverse()[source]¶

multiply_by_negative(x: Term, proof_x_is_negative: GreaterThan | LessThan) → GreaterThan[source]¶

multiply_by_positive(x: Term, proof_x_is_positive: GreaterThan | LessThan) → GreaterThan[source]¶

name: str = 'GreaterThan'¶

p_multiply_by_negative(x: Term, proof_x_is_negative: GreaterThan | LessThan) → GreaterThan[source]¶: Logical inference rule. Same as multiply_by_negative, but returns a proven proposition

p_multiply_by_positive(x: Term, proof_x_is_positive: GreaterThan | LessThan) → GreaterThan[source]¶: Logical inference rule. Same as multiply_by_positive, but returns a proven proposition

p_to_less_than()[source]¶: Logical inference rule. Same as to_less_than, but returns a proven proposition

to_less_than()[source]¶: If self is of the form a > b, returns an inequality of the form b < a

to_negative_inequality()[source]¶: If self is of the form a > b, returns an inequality of the form b - a < 0

to_positive_inequality()[source]¶: If self is of the form a > b, returns an inequality of the form a - b > 0

pylogic.proposition.ordering.greaterthan.is_absolute(expr: Term, expr_not_zero: Not[Equals]) → GreaterThan[source]¶: Logical inference rule. Given an expr of the form sympy.Abs(x) and a proof that the expr is not zero, return a proven proposition that says sympy.Abs(x) > 0

pylogic.proposition.ordering.greaterthan.is_even_power(expr: Any) → GreaterThan[source]¶: Logical inference rule. Given an expr of the form x**(2n), return a proven proposition that says x**(2n) > 0

pylogic.proposition.ordering.greaterthan.is_rational_power(expr: Any, proof_base_is_positive: GreaterThan) → GreaterThan[source]¶: Logical inference rule. Given an expr of the form x**(p/q) and a proof that x > 0, return a proven proposition that says x**(p/q) > 0

pylogic.proposition.ordering.inference module¶

pylogic.proposition.ordering.inference.transitive(conclusion_type: ConcType, *props) → BinaryRelation[source]¶

Logical inference rule. Prove a relation from a series of relations using transitivity.

For example, if we have a series of relations: a = b, b <= c, c < d, d = e we can prove a < e (if conclusion type is <) or a <= e (if conclusion type is <=).

pylogic.proposition.ordering.lessorequal module¶

class pylogic.proposition.ordering.lessorequal.LessOrEqual(left: T, right: U, is_assumption: bool = False, description: str = '', name=None, **kwargs)[source]¶

Bases: TotalOrder[T, U], _Ordering

add_negative_to_left(negative: Any) → LessThan[source]¶: Logical inference rule. If self is of the form a <= b and c is negative, returns a proposition of the form a + c < b

add_nonnegative_to_right(nonnegative: Any) → LessOrEqual[source]¶: Logical inference rule. If self is of the form a <= b and c is nonnegative, returns a proposition of the form a <= b + c

add_nonpositive_to_left(nonpositive: Any) → LessOrEqual[source]¶: Logical inference rule. If self is of the form a <= b and c is nonpositive (c <= 0), returns a proposition of the form a + c <= b

add_positive_to_right(positive: Any) → LessThan[source]¶: Logical inference rule. If self is of the form a <= b and c is positive, returns a proposition of the form a < b + c

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.

infix_symbol: str = '<='¶

infix_symbol_latex: str = '\\leq'¶

name: str = 'LessOrEqual'¶

to_disjunction() → Or[LessThan, Equals][source]¶: If self is of the form a <= b, returns a proposition of the form a < b or a = b

pylogic.proposition.ordering.lessthan module¶

class pylogic.proposition.ordering.lessthan.LessThan(left: T, right: U, is_assumption: bool = False, description: str = '', name=None, **kwargs)[source]¶

Bases: StrictTotalOrder[T, U], _Ordering

add_nonnegative_to_right(nonnegative: Any) → LessThan[source]¶: Logical inference rule. If self is of the form a < b and c is nonnegative, returns a proposition of the form a < b + c

add_nonpositive_to_left(nonpositive: Any) → LessThan[source]¶: Logical inference rule. If self is of the form a < b and c is nonpositive (c <= 0), returns a proposition of the form a + c < b

by_definition() → LessThan[source]¶: Logical inference rule. Determine if the proposition is true 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.

infix_symbol: str = '<'¶

infix_symbol_latex: str = '<'¶

mul_inverse()[source]¶

multiply_by_negative(x: Term, proof_x_is_negative: GreaterThan | LessThan) → LessThan[source]¶

multiply_by_positive(x: Term, proof_x_is_positive: GreaterThan | LessThan) → LessThan[source]¶

name: str = 'LessThan'¶

p_multiply_by_negative(x: Term, proof_x_is_negative: GreaterThan | LessThan) → LessThan[source]¶: Logical inference rule. Same as multiply_by_negative, but returns a proven proposition

p_multiply_by_positive(x: Term, proof_x_is_positive: GreaterThan | LessThan) → LessThan[source]¶: Logical inference rule. Same as multiply_by_positive, but returns a proven proposition

p_to_greater_than()[source]¶: Logical inference rule. Same as to_greater_than, but returns a proven proposition

to_greater_than()[source]¶: If self is of the form a < b, returns an inequality of the form b > a

to_negative_inequality()[source]¶: If self is of the form a < b, returns an inequality of the form a - b < 0

to_positive_inequality()[source]¶: If self is of the form a < b, returns an inequality of the form b - a > 0

pylogic.proposition.ordering.ordering module¶

pylogic.proposition.ordering.partial module¶

class pylogic.proposition.ordering.partial.PartialOrder(left: T, right: U, name: str = 'PartialOrder', is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: BinaryRelation[T, U], _Ordering

Parameters:

name (str) – The name of the partial order.
left (T) – The left term of the partial order.
right (U) – The right term of the partial order.
BinaryRelation. (Also receives the same parameters as)

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.

infix_symbol: str = '<='¶

infix_symbol_latex: str = '\\leq'¶

is_antisymmetric: bool = True¶

is_reflexive: bool = True¶

is_transitive: bool = True¶

name: str = 'PartialOrder'¶

to_sympy()[source]¶

class pylogic.proposition.ordering.partial.StrictPartialOrder(left: T, right: U, name: str = 'StrictPartialOrder', is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: BinaryRelation[T, U], _Ordering

Parameters:

name (str) – The name of the strict partial order.
left (T) – The left term of the strict partial order.
right (U) – The right term of the strict partial order.
BinaryRelation. (Also receives the same parameters as)

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.

infix_symbol: str = '<'¶

infix_symbol_latex: str = '<'¶

is_asymmetric: bool = True¶

is_irreflexive: bool = True¶

is_transitive: bool = True¶

name: str = 'StrictPartialOrder'¶

to_sympy()[source]¶

pylogic.proposition.ordering.theorems module¶

pylogic.proposition.ordering.theorems.absolute_value_nonnegative_f(x: Term) → Or[GreaterThan, Equals][source]¶: Logical inference rule. If x is a real number, returns a proven proposition of the form Abs(x) > 0 V Abs(x) = 0.

pylogic.proposition.ordering.theorems.order_axiom_bf(x: UnevaluatedExpr | Numeric, y: UnevaluatedExpr | Numeric) → Implies[Equals, Not[LessThan]][source]¶
pylogic.proposition.ordering.theorems.order_axiom_bf(x: sp.Basic | Numeric, y: sp.Basic | Numeric) → Implies[Equals, Not[LessThan]]

pylogic.proposition.ordering.total module¶

class pylogic.proposition.ordering.total.StrictTotalOrder(left: T, right: U, name: str = 'StrictPartialOrder', is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: StrictPartialOrder[T, U]

infix_symbol: str = '<'¶

infix_symbol_latex: str = '<'¶

is_connected: bool = True¶

name: str = 'StrictTotalOrder'¶

class pylogic.proposition.ordering.total.TotalOrder(left: T, right: U, name: str = 'PartialOrder', is_assumption: bool = False, description: str = '', **kwargs)[source]¶

Bases: PartialOrder[T, U]

infix_symbol: str = '<='¶

infix_symbol_latex: str = '\\leq'¶

is_strongly_connected: bool = True¶

name: str = 'TotalOrder'¶