pylogic package¶
Subpackages¶
- pylogic.enviroment_settings package
- pylogic.expressions package
- Submodules
- pylogic.expressions.abs module
- pylogic.expressions.expr module
Add
BinaryExpression
CustomExpr
Expr
Expr.atoms
Expr.copy()
Expr.deepcopy()
Expr.doit()
Expr.equals()
Expr.eval_same()
Expr.evaluate()
Expr.is_atomic
Expr.is_even
Expr.is_finite
Expr.is_in()
Expr.is_integer
Expr.is_list
Expr.is_natural
Expr.is_negative
Expr.is_nonnegative
Expr.is_nonpositive
Expr.is_nonzero
Expr.is_not_in()
Expr.is_odd
Expr.is_positive
Expr.is_rational
Expr.is_real
Expr.is_sequence
Expr.is_set
Expr.is_zero
Expr.kwargs
Expr.mutable_attrs_to_copy
Expr.replace()
Expr.symbols
Expr.to_sympy()
Expr.unify()
Expr.update_properties()
Mul
Pow
add()
cbrt()
distance()
div()
max()
mul()
replace()
sqrt()
sub()
to_sympy()
- pylogic.expressions.function module
- pylogic.expressions.gcd module
- pylogic.expressions.limit module
- pylogic.expressions.max module
- pylogic.expressions.min module
- pylogic.expressions.mod module
- pylogic.expressions.piecewise module
- pylogic.expressions.prod module
- pylogic.expressions.sequence_term module
- pylogic.expressions.sum module
- Module contents
- pylogic.infix package
- pylogic.printing package
- pylogic.proposition package
- Subpackages
- pylogic.proposition.ordering package
- Submodules
- pylogic.proposition.ordering.greaterorequal module
- pylogic.proposition.ordering.greaterthan module
- pylogic.proposition.ordering.inference module
- pylogic.proposition.ordering.lessorequal module
- pylogic.proposition.ordering.lessthan module
- pylogic.proposition.ordering.ordering module
- pylogic.proposition.ordering.partial module
- pylogic.proposition.ordering.theorems module
- pylogic.proposition.ordering.total module
- Module contents
- pylogic.proposition.quantified package
- pylogic.proposition.relation package
- pylogic.proposition.ordering package
- Submodules
- pylogic.proposition.and_ module
- pylogic.proposition.contradiction module
- pylogic.proposition.exor module
- pylogic.proposition.iff module
- pylogic.proposition.implies module
Implies
Implies.as_text()
Implies.contrapositive()
Implies.copy()
Implies.deepcopy()
Implies.definite_clause_resolve()
Implies.describe()
Implies.first_unit_definite_clause_resolve()
Implies.has_as_subproposition()
Implies.hypothetical_syllogism()
Implies.impl_elim()
Implies.replace()
Implies.to_sympy()
Implies.unify()
Implies.unit_definite_clause_resolve()
InferenceRule
- pylogic.proposition.not_ module
- pylogic.proposition.or_ module
- pylogic.proposition.proof_search module
- pylogic.proposition.proposition module
InferenceRule
Proposition
Proposition.name
Proposition.is_assumption
Proposition.is_axiom
Proposition.description
Proposition.args
Proposition.arity
Proposition.is_proven
Proposition.from_assumptions
Proposition.deduced_from
Proposition.and_()
Proposition.and_reverse()
Proposition.as_text()
Proposition.assume()
Proposition.atoms
Proposition.by_inspection()
Proposition.by_inspection_check()
Proposition.close_all_scopes()
Proposition.contradicts()
Proposition.copy()
Proposition.de_morgan()
Proposition.deepcopy()
Proposition.definition
Proposition.describe()
Proposition.eval_same()
Proposition.followed_from()
Proposition.has_as_subproposition()
Proposition.iff()
Proposition.implies()
Proposition.inference_rules()
Proposition.is_one_of()
Proposition.is_proven
Proposition.is_special_case_of()
Proposition.modus_ponens()
Proposition.modus_tollens()
Proposition.mp()
Proposition.mt()
Proposition.or_()
Proposition.or_reverse()
Proposition.p_and()
Proposition.p_and_reverse()
Proposition.p_substitute()
Proposition.replace()
Proposition.set_desc()
Proposition.set_description()
Proposition.substitute()
Proposition.symbols
Proposition.thus_forall()
Proposition.thus_there_exists()
Proposition.todo()
Proposition.unify()
Proposition.xor()
Proposition.xor_reverse()
get_assumptions()
pred()
predicate()
predicates()
preds()
prop()
proposition()
propositions()
props()
- Module contents
- Subpackages
- pylogic.structures package
- Subpackages
- pylogic.structures.grouplike package
- pylogic.structures.ringlike package
- Submodules
- pylogic.structures.ringlike.commutative_ring module
- pylogic.structures.ringlike.crooked_semiring module
- pylogic.structures.ringlike.crooked_semirng module
- pylogic.structures.ringlike.division_ring module
- pylogic.structures.ringlike.field module
- pylogic.structures.ringlike.left_ringoid module
- pylogic.structures.ringlike.nearring module
- pylogic.structures.ringlike.ordered_field module
- pylogic.structures.ringlike.right_ringoid module
- pylogic.structures.ringlike.ring module
- pylogic.structures.ringlike.ringoid module
- pylogic.structures.ringlike.rng module
- pylogic.structures.ringlike.semiring module
- pylogic.structures.ringlike.semirng module
- Module contents
- Submodules
- pylogic.structures.class_ module
- pylogic.structures.collection module
- pylogic.structures.ordered_set module
OrderedSet
OrderedSet.add_to_both_sides_of_inequality
OrderedSet.order_definition
OrderedSet.order_is_antisymmetric
OrderedSet.order_is_reflexive
OrderedSet.order_is_strongly_connected
OrderedSet.order_is_transitive
OrderedSet.product_of_nonnegatives_is_nonnegative
OrderedSet.property_add_to_both_sides_of_inequality()
OrderedSet.property_order_definition()
OrderedSet.property_order_is_antisymmetric()
OrderedSet.property_order_is_reflexive()
OrderedSet.property_order_is_strongly_connected()
OrderedSet.property_order_is_transitive()
OrderedSet.property_product_of_nonnegatives_is_nonnegative()
OrderedSet.property_strict_order_definition()
OrderedSet.property_strict_order_is_asymmetric()
OrderedSet.property_strict_order_is_connected()
OrderedSet.property_strict_order_is_irreflexive()
OrderedSet.property_strict_order_is_transitive()
OrderedSet.strict_order_definition
OrderedSet.strict_order_is_asymmetric
OrderedSet.strict_order_is_connected
OrderedSet.strict_order_is_irreflexive
OrderedSet.strict_order_is_transitive
OrderedSet.strict_total_order
OrderedSet.total_order
- pylogic.structures.sequence module
FiniteSequence
Pair
PeriodicSequence
Sequence
Sequence.contains()
Sequence.define_predicate()
Sequence.equals()
Sequence.evaluate()
Sequence.is_atomic
Sequence.is_even
Sequence.is_finite
Sequence.is_in()
Sequence.is_integer
Sequence.is_list
Sequence.is_natural
Sequence.is_negative
Sequence.is_nonnegative
Sequence.is_nonpositive
Sequence.is_nonzero
Sequence.is_not_in()
Sequence.is_odd
Sequence.is_positive
Sequence.is_rational
Sequence.is_real
Sequence.is_sequence
Sequence.is_set
Sequence.is_zero
Sequence.predicate()
Sequence.replace()
Sequence.to_sympy()
Triple
sequences()
- pylogic.structures.set_ module
CartesPower
CartesProduct
Complement
Difference
FiniteCartesProduct
FiniteIntersection
FiniteSet
FiniteUnion
Intersection
SeqSet
Set
Set.containment_function()
Set.contains()
Set.copy()
Set.countable()
Set.deepcopy()
Set.dummy_eq()
Set.equals()
Set.eval_same()
Set.evaluate()
Set.illegal_occur_check()
Set.illegal_occur_check_pred()
Set.is_atomic
Set.is_even
Set.is_finite
Set.is_integer
Set.is_list
Set.is_natural
Set.is_negative
Set.is_nonnegative
Set.is_nonpositive
Set.is_nonzero
Set.is_odd
Set.is_positive
Set.is_rational
Set.is_real
Set.is_sequence
Set.is_set
Set.is_subset_of()
Set.is_zero
Set.kwargs
Set.level
Set.mutable_attrs_to_copy
Set.predicate()
Set.replace()
Set.to_sympy()
Union
sets()
- Module contents
- Subpackages
- pylogic.syntax_helpers package
- pylogic.theories package
- Submodules
- pylogic.theories.integers module
- pylogic.theories.natural_numbers module
NaturalsSemiring
NaturalsSemiring.closed_under_successor
NaturalsSemiring.divides()
NaturalsSemiring.even()
NaturalsSemiring.odd()
NaturalsSemiring.prime()
NaturalsSemiring.property_closed_under_successor()
NaturalsSemiring.property_strong_induction_formal()
NaturalsSemiring.property_successor_injective()
NaturalsSemiring.property_successor_neq_0()
NaturalsSemiring.property_well_ordering_set()
NaturalsSemiring.property_zero_is_min_nat()
NaturalsSemiring.strong_induction()
NaturalsSemiring.strong_induction_formal
NaturalsSemiring.successor
NaturalsSemiring.successor_injective
NaturalsSemiring.successor_neq_0
NaturalsSemiring.weak_induction()
NaturalsSemiring.well_ordering()
NaturalsSemiring.well_ordering_set
NaturalsSemiring.zero_is_min_nat
Prime
- pylogic.theories.numbers module
- pylogic.theories.rational_numbers module
- pylogic.theories.real_numbers module
- Module contents
- pylogic.typing package
Submodules¶
pylogic.abc module¶
pylogic.assumptions_context module¶
- class pylogic.assumptions_context.AssumptionsContext(name: str | None = None)[source]¶
Bases:
object
- get_first_proven() Proposition | None [source]¶
Returns the first proven proposition after the context.
- get_proven()[source]¶
Returns a list of implications that have been proven as a result of closing this context.
Example: ``` p = Proposition(“p”) q = Proposition(“q”) r = Proposition(“r”) p_implies_q = p.implies(q).assume() q_implies_r = q.implies(r).assume() with AssumptionsContext() as ctx:
p_true = p.assume() r_true = p_true.modus_ponens(p_implies_q).modus_ponens(q_implies_r) conclude(r_true)
- pylogic.assumptions_context.conclude(conclusion: Proposition) Proposition [source]¶
Used inside a context.
Tell pylogic that you are interested in proving an implication or a Forall statement incolving this conclusion when the context is closed.
- pylogic.assumptions_context.context_variables(name: str, **kwargs) Variable [source]¶
- pylogic.assumptions_context.context_variables(*names: str, **kwargs) tuple[Variable, ...]
- pylogic.assumptions_context.ctx_vars(name: str, **kwargs) Variable [source]¶
- pylogic.assumptions_context.ctx_vars(*names: str, **kwargs) tuple[Variable, ...]
- pylogic.assumptions_context.to_prove(*target: Proposition) Proposition | None [source]¶
Set a target proposition to prove.
When called with no arguments, it returns the current target proposition.
pylogic.constant module¶
pylogic.helpers module¶
- class pylogic.helpers.Getter(key, value: T | None = None)¶
Bases:
Generic
[T
]Get the actual key object reference in a dict/set when its value is equal to some other object. from https://stackoverflow.com/a/78219110/22426744
- key¶
- value¶
- class pylogic.helpers.Namespace(dict_: dict[str, Any] | None = None, **kwargs: Any)¶
Bases:
SimpleNamespace
Attributes can be accessed using dot notation or dictionary subscript notation.
- pylogic.helpers.Rational(numerator: Term | PythonNumeric, denominator: Term | PythonNumeric) Constant[Fraction] ¶
- pylogic.helpers.assume(arg: P, *args: Unpack[Ps]) P | tuple[P, Unpack[Ps]] ¶
- pylogic.helpers.copy(obj: T) T ¶
Creates a shallow copy of the object if object is not numeric.
- Raises:
AttributeError "obj has no attribute copy" if obj is neither numeric nor a pylogic object. –
- pylogic.helpers.deepcopy(obj: T) T ¶
Creates a deep copy of the object if object is not numeric.
- Raises:
AttributeError "obj has no attribute deepcopy" if obj is neither numeric nor a pylogic object. –
- pylogic.helpers.eval_same(x: Any, y: Any) bool ¶
Check if x and y evaluate to the same value.
- pylogic.helpers.find_first(predicate: Callable[[T], bool], args: Iterable[T]) tuple[int, T] | tuple[None, None] ¶
Find the first element in args that satisfies the predicate.
- pylogic.helpers.get_class_ns(expr: Any) set[Class] ¶
Get all class{n} in expr.
- pylogic.helpers.getkey(keyed: ~typing.Container, key: ~pylogic.helpers.T, default=<object object>) T ¶
- pylogic.helpers.has_been_proven(to_prove: Proposition, proven: Proposition) bool ¶
Check if to_prove is equal to proven, and proven is proven.
- pylogic.helpers.is_integer_numeric(*args: Any) bool ¶
Check if the arguments are of integer numeric types.
- pylogic.helpers.is_iterable(obj: Any) bool ¶
Check if the object is iterable.
- pylogic.helpers.is_numeric(*args: Any) bool ¶
Check if the arguments are of numeric types.
- pylogic.helpers.is_python_numeric(*args: Any) bool ¶
Check if the arguments are of Python numeric types.
- pylogic.helpers.is_python_real_numeric(*args: Any) bool ¶
Check if the arguments are of Python real numeric types.
- pylogic.helpers.latex(arg: Any) str ¶
- pylogic.helpers.python_to_pylogic(arg: Any) Proposition | Expr | Symbol | Sequence | Set ¶
Convert certain python objects to Pylogic objects. A Python character/str with one character is converted to a Pylogic Constant. A Python set is converted to a Pylogic Set. A Python dictionary is converted to a Pylogic Set of Pairs. A Python tuple is converted to a Pylogic Pair, Triple, or Sequence. A Python int, float, Fraction, complex, or Decimal is converted to a Pylogic Constant. A Python iterable (str included) besides those above is converted to a Pylogic Sequence.
Raises TypeError if arg is not one of the above.
- pylogic.helpers.replace(expr, replace_dict: dict, equal_check: Callable | None = None, positions: list[list[int]] | None = None) Any ¶
- pylogic.helpers.ternary_and(*vals: bool | None) bool | None ¶
- pylogic.helpers.ternary_if_not_none(val: bool | None, default: bool | None) bool | None ¶
- pylogic.helpers.ternary_not(val: bool | None) bool | None ¶
- pylogic.helpers.ternary_or(*val1: bool | None) bool | None ¶
- pylogic.helpers.todo(arg: P, *args: Unpack[Ps]) P | tuple[P, Unpack[Ps]] ¶
- pylogic.helpers.try_except(func: Callable[[...], T], exc_to_ignore: tuple[Exception, ...] = (), exc_to_raise: Exception | None = None, cleanup: Callable[[], None] | None = None, *args: Any, **kwargs: Any) T | None ¶
Try to run a function and return the result if successful. If any of exc_to_ignore is encountered, raise exc_to_raise (if exc_to_raise not None) or return None (if None). If exc_to_ignore is empty, it raises all exceptions.
- pylogic.helpers.type_check(arg: Any, *types: type, context: Any = None) Literal[True] ¶
Check if arg is an instance of any of the types.
Raises TypeError if arg is not an instance of any of the types.
- pylogic.helpers.type_check_no(arg: Any, *types: type, context: Any = None) Literal[True] ¶
Assert that arg is not an instance of any of the types.
Raises TypeError if arg is an instance of any of the types.
- pylogic.helpers.unify(a: Proposition | Term, b: Proposition | Term) Unification | Literal[True] | None ¶
Unification algorithm.
pylogic.inference module¶
- class pylogic.inference.Inference(starting_premise: T | None, *other_premises: Unpack[Props], rule: str = 'given')¶
Bases:
Generic
[T
,Unpack
[Props
]]Represents an inference in a proof.
- Raises:
InvalidRuleError – if the rule is not in the set of valid rules
- exception pylogic.inference.InvalidRuleError(rule: str)¶
Bases:
Exception
pylogic.symbol module¶
- class pylogic.symbol.Symbol(*args, **kwargs)[source]¶
Bases:
object
- contains(other: Term, **kwargs) IsContainedIn [source]¶
- property first_second: tuple[Self, Self]¶
if self has is_pair True, return two variables representing the first and second elements of self. Otherwise, raise a ValueError
- is_atomic = True¶
- property is_even: bool | None¶
- property is_finite: bool | None¶
- is_in(other: Set | Variable | Class | SequenceTerm[S], **kwargs) IsContainedIn [source]¶
- property is_integer: bool | None¶
- property is_list: bool | None¶
- property is_natural: bool | None¶
- property is_negative: bool | None¶
- property is_nonnegative: bool | None¶
- property is_nonpositive: bool | None¶
- property is_nonzero: bool | None¶
- is_not_in(other: Set | Variable | Class | SequenceTerm[S], **kwargs) Not[IsContainedIn] [source]¶
- property is_odd: bool | None¶
- property is_positive: bool | None¶
- property is_rational: bool | None¶
- property is_real: bool | None¶
- property is_sequence: bool | None¶
- property is_set: bool | None¶
- is_subset_of(other: Symbol | Set, **kwargs) IsSubsetOf [source]¶
- property is_zero: bool | None¶
- kwargs = [('name', 'name'), ('_from_existential_instance', '_from_existential_instance'), ('knowledge_base', 'knowledge_base'), ('real', '_is_real'), ('rational', '_is_rational'), ('integer', '_is_integer'), ('natural', '_is_natural'), ('zero', '_is_zero'), ('nonpositive', '_is_nonpositive'), ('nonnegative', '_is_nonnegative'), ('even', '_is_even'), ('sequence', '_is_sequence'), ('finite', '_is_finite'), ('length', 'length'), ('positive', '_is_positive'), ('negative', '_is_negative'), ('set', '_is_set'), ('list', '_is_list'), ('graph', 'is_graph'), ('pair', 'is_pair'), ('list_', 'is_list_'), ('latex_name', 'latex_name'), ('depends_on', 'depends_on'), ('sets_contained_in', 'sets_contained_in')]¶
- mutable_attrs_to_copy = ['properties_of_each_term', 'independent_dependencies']¶
- property nodes_edges: tuple[Self, Self]¶
if self has is_graph True, return two variables representing the nodes and edges of self. Otherwise, raise a ValueError
- replace(replace_dict: dict, equal_check: Callable | None = None, positions: list[list[int]] | None = None) Any [source]¶
Replace occurences of old with new in the object, where replace_dict = {old: new}. If equal_check is provided, it should be a function that takes two arguments and returns True if they are equal.
pylogic.sympy_helpers module¶
- class pylogic.sympy_helpers.PylSympyExpr(*args)¶
Bases:
CustomExpr
- default_assumptions = {}¶
- name = 'PylSympyExpr'¶
- class pylogic.sympy_helpers.PylSympyExprCondPair(*args, _pyl_class: type | None = None, _pyl_init_args: tuple | None = None, _pyl_init_kwargs: dict[str, Any] | None = None, **kwargs)¶
Bases:
ExprCondPair
- default_assumptions = {}¶
- class pylogic.sympy_helpers.PylSympyFunction(*args, _pyl_class: type | None = None, _pyl_init_args: tuple | None = None, _pyl_init_kwargs: dict[str, Any] | None = None, **kwargs)¶
Bases:
UndefinedFunction
- class pylogic.sympy_helpers.PylSympySeqBase(*args, _pyl_class: type | None = None, _pyl_init_args: tuple | None = None, _pyl_init_kwargs: dict[str, Any] | None = None, **kwargs)¶
Bases:
SeqBase
- default_assumptions = {'commutative': True}¶
- is_commutative: bool | None = True¶
- class pylogic.sympy_helpers.PylSympySeqFormula(*args, _pyl_class: type | None = None, _pyl_init_args: tuple | None = None, _pyl_init_kwargs: dict[str, Any] | None = None, **kwargs)¶
Bases:
SeqFormula
- default_assumptions = {'commutative': True}¶
- is_commutative: bool | None = True¶
- class pylogic.sympy_helpers.PylSympySet(*args, _pyl_class: type | None = None, _pyl_init_args: tuple | None = None, _pyl_init_kwargs: dict[str, Any] | None = None, **kwargs)¶
Bases:
Set
- default_assumptions = {}¶
- class pylogic.sympy_helpers.PylSympySymbol(*args, _pyl_class: type | None = None, _pyl_init_args: tuple | None = None, _pyl_init_kwargs: dict[str, Any] | None = None, **kwargs)¶
Bases:
Symbol
- default_assumptions = {}¶
- name: str¶
- pylogic.sympy_helpers.sympy_to_pylogic(expr: Integer) Constant[int] [source]¶
- pylogic.sympy_helpers.sympy_to_pylogic(expr: Float) Constant[float]
- pylogic.sympy_helpers.sympy_to_pylogic(expr: Rational) Constant[Fraction]
- pylogic.sympy_helpers.sympy_to_pylogic(expr: Add) Add
- pylogic.sympy_helpers.sympy_to_pylogic(expr: Mul) Mul
- pylogic.sympy_helpers.sympy_to_pylogic(expr: Pow) Pow
- pylogic.sympy_helpers.sympy_to_pylogic(expr: Abs) Abs
- pylogic.sympy_helpers.sympy_to_pylogic(expr: SeqFormula) Sequence
- pylogic.sympy_helpers.sympy_to_pylogic(expr: SeqPer) PeriodicSequence
- pylogic.sympy_helpers.sympy_to_pylogic(expr: Set) Set
- pylogic.sympy_helpers.sympy_to_pylogic(expr: Symbol) Symbol
- pylogic.sympy_helpers.sympy_to_pylogic(expr: Expr) CustomExpr
Can only convert sympy expressions that are supported by pylogic.
pylogic.variable module¶
- class pylogic.variable.Variable(*args, depends_on: tuple[Variable, ...] = (), **kwargs)[source]¶
Bases:
Symbol