pylogic package

Subpackages

Submodules

pylogic.abc module

pylogic.assumptions_context module

class pylogic.assumptions_context.AssumptionsContext(name: str | None = None)[source]

Bases: object

close()[source]
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)

print(ctx.get_proven()) ` Output: ` [p -> r] ```

open()[source]
var(*args, **kwargs) Variable[source]
variable(*args, **kwargs) Variable[source]
variables(name: str, **kwargs) Variable[source]
variables(*names: str, **kwargs) tuple[Variable, ...]
vars(name: str, **kwargs) Variable[source]
vars(**kwargs) tuple[Variable, ...]
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_variable(*args, **kwargs) Variable[source]
pylogic.assumptions_context.context_variables(name: str, **kwargs) Variable[source]
pylogic.assumptions_context.context_variables(*names: str, **kwargs) tuple[Variable, ...]
pylogic.assumptions_context.ctx_var(*args, **kwargs) Variable[source]
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

class pylogic.constant.Constant(value: T, *args, **kwargs)[source]

Bases: Symbol, Generic[T]

copy() Self[source]

Create a copy of this symbol.

deepcopy() Self[source]
to_decimal() Decimal[source]
to_fraction() Fraction[source]
to_sympy() sp.Integer[source]
to_sympy() sp.Float
to_sympy() sp.Add
to_sympy() sp.Rational
to_sympy() sp.Float
to_sympy() sp.Symbol
pylogic.constant.constants(value: T, **kwargs) Constant[T][source]
pylogic.constant.constants(*args: T, **kwargs) tuple[Constant[T], ...]

Create multiple Constant instances at once.

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]
class pylogic.helpers.Side(value)

Bases: Enum

LEFT = 1
RIGHT = 2
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.get_consts(expr: Any) set[Constant]
pylogic.helpers.get_sets(expr: Any) set[Set]

Get all sets in expr.

pylogic.helpers.get_vars(expr: Any) set[Variable]

Get all variables 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_prime(num: int | Fraction | Constant[int] | Constant[Fraction]) bool
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]
copy() Self[source]

Create a copy of this symbol.

deepcopy() Self[source]
equals(other: Symbol | PythonNumeric | Expr | Set, **kwargs) Equals[source]
eval_same(other: Any) bool[source]

Check if two symbols evaluate to the same value.

evaluate(**kwargs) Self[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

get_independent_dependencies() tuple[Variable, ...][source]
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.

property size: Self | Constant
to_sympy() Symbol[source]
pylogic.symbol.symbols(*args, **kwargs)[source]

pylogic.sympy_helpers module

exception pylogic.sympy_helpers.FromSympyError[source]

Bases: ValueError

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
exception pylogic.sympy_helpers.ToSympyError[source]

Bases: ValueError

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

pylogic.variable.Var

alias of Variable

class pylogic.variable.Variable(*args, depends_on: tuple[Variable, ...] = (), **kwargs)[source]

Bases: Symbol

containment_function(x: Any) bool[source]

For variable sets.

contains(x: Any, **kwargs) Any[source]

For variable sets.

countable(is_assumption: bool = False, **kwargs) Any[source]
predicate(x: Any) Any[source]

For variable sets.

unbind() None[source]
pylogic.variable.unbind(*variables: Variable) None[source]

Unbinds variables. This indicates that they are no longer bound to a quantifier and can be reused in nested quantified statements.

pylogic.variable.variables(name: str, **kwargs) Variable[source]
pylogic.variable.variables(*names: str, **kwargs) tuple[Variable, ...]

Creates variables.

pylogic.warn module

exception pylogic.warn.PylogicInternalWarning[source]

Bases: Warning

Module contents