core

And

Bases: _TwoPlaceConnective

A class representing logical conjunction

Attributes:

Name	Type	Description
a		the left hand part of the conjunction
b		the right hand part of the conjunction

Source code in src\logicalpy\core.py

class And(_TwoPlaceConnective):
    """A class representing logical conjunction

    Attributes:
        a: the left hand part of the conjunction
        b: the right hand part of the conjunction
    """

    CONNECTIVE_SYMBOL = "∧"
    LATEX_SYMBOL = r"\land"

    def is_satisfied(self, valuation: dict[str, bool]) -> bool:
        return self.a.is_satisfied(valuation) and self.b.is_satisfied(valuation)

    def _distribute_and_over_or(self):
        if isinstance(self.b, Or):
            return Or(
                And(self.a, self.b.a)._distribute_and_over_or(),
                And(self.a, self.b.b)._distribute_and_over_or(),
            )
        elif isinstance(self.a, Or):
            return Or(
                And(self.b, self.a.a)._distribute_and_over_or(),
                And(self.b, self.a.b)._distribute_and_over_or(),
            )
        else:
            return And(
                self.a._distribute_and_over_or(),
                self.b._distribute_and_over_or(),
            )

BiImplies

Bases: _TwoPlaceConnective

A class representing logical bi-implication (also called biconditional)

Attributes:

Name	Type	Description
a		the left hand part of the biconditional
b		the right hand part of the biconditional

Source code in src\logicalpy\core.py

class BiImplies(_TwoPlaceConnective):
    """A class representing logical bi-implication (also called biconditional)

    Attributes:
        a: the left hand part of the biconditional
        b: the right hand part of the biconditional
    """

    CONNECTIVE_SYMBOL = "↔"
    LATEX_SYMBOL = r"\leftrightarrow"

    def is_satisfied(self, valuation: dict[str, bool]) -> bool:
        return self.a.is_satisfied(valuation) == self.b.is_satisfied(valuation)

    def _eliminate_conditionals(self):
        a = self.a._eliminate_conditionals()
        b = self.b._eliminate_conditionals()
        return And(Or(Not(a), b), Or(Not(b), a))

Formula

The general class for a propositional formula

Attributes:

Name	Type	Description
formula		the formula described (can be an instance of any of the base connective classes)

Examples:

>>> from logicalpy import Proposition, Or, Not, Formula
>>> P = Proposition("P")
>>> test_formula = Formula(Or(P, Not(P)))
>>> str(test_formula)
'P ∨ ¬P'
>>> test_formula.propositions()
{'P'}
>>> test_formula.is_satisfied({"P": True})
True
>>> print(Formula.from_string("P & (P -> P)")
P ∧ (P → P)

Source code in src\logicalpy\core.py

class Formula:
    """The general class for a propositional formula

    Attributes:
        formula: the formula described (can be an instance of any of the base connective classes)

    Examples:
        >>> from logicalpy import Proposition, Or, Not, Formula
        >>> P = Proposition("P")
        >>> test_formula = Formula(Or(P, Not(P)))
        >>> str(test_formula)
        'P ∨ ¬P'
        >>> test_formula.propositions()
        {'P'}
        >>> test_formula.is_satisfied({"P": True})
        True
        >>> print(Formula.from_string("P & (P -> P)")
        P ∧ (P → P)

    """

    def __init__(self, formula, /):
        """The formula's constructor

        Args:
            formula: the formula represented (can be an instance of any of the base connective classes)

        """
        self._formula = formula

    def __str__(self) -> str:
        formula_str = str(self._formula)
        if formula_str.startswith("(") and formula_str.endswith(
            ")"
        ):  # if there are outer parenthesis, we remove them
            return formula_str[1:-1]
        return formula_str

    def __eq__(self, other) -> bool:
        if isinstance(other, Formula):
            return self._formula == other._formula
        return False

    def __repr__(self) -> str:
        return f"Formula({repr(self._formula)})"

    def __hash__(self) -> int:
        return hash(str(self))

    def to_latex(self) -> str:
        """Renders the formula as LaTeX code

        Returns:
            (str): the LaTeX representation of the formula, as inline math

        """
        formula_latex = self._formula.to_latex()
        if formula_latex.startswith("(") and formula_latex.endswith(
            ")"
        ):  # if there are outer parenthesis, we remove them
            return "$" + formula_latex[1:-1] + "$"
        return "$" + formula_latex + "$"

    @classmethod
    def from_string(cls, formula_str: str):
        """Builds a formula from a string representation of it

        Args:
            formula_str (str): the string containing the string representation of the formula

        Returns:
            (Formula): the formula built

        """
        return cls(_interpret_formula_tree(PROPOSITIONAL_PARSER.parse(formula_str)))

    def propositions(self) -> set[str]:
        """A method for listing all the propositions of the formula

        Returns:
            (set[str]): the set of all the propositions of the formula, each represented by its name (str)

        """
        return self._formula.propositions()

    def is_satisfied(self, valuation: dict[str, bool]) -> bool:
        """Tests whether the formula is satisfied by the truth valuation given

        Args:
            valuation (dict[str, bool]): a dictionary associating each proposition name (str) with a truth value (bool)

        Returns:
            (bool): True is the formula is satisfied by the truth valuation given, and False otherwise

        Raises:
            ValueError: if the truth value of one of the formula's propositions isn't precised in the valuation given

        """
        return self._formula.is_satisfied(valuation)

    def is_literal(self) -> bool:
        """Tests whether the formula is a literal, i.e. a proposition or its negation"""
        if isinstance(self._formula, Proposition):
            return True
        elif isinstance(self._formula, Not):
            if isinstance(self._formula.a, Proposition):
                return True
        return False

    def is_proposition(self) -> bool:
        """Tests whether the formula is only a proposition"""
        return isinstance(self._formula, Proposition)

    def is_negation(self) -> bool:
        """Tests whether the formula's main connective is a negation"""
        return isinstance(self._formula, Not)

    def is_conjunction(self) -> bool:
        """Tests whether the formula's main connective is a conjunction"""
        return isinstance(self._formula, And)

    def is_disjunction(self) -> bool:
        """Tests whether the formula's main connective is a disjunction"""
        return isinstance(self._formula, Or)

    def is_implication(self) -> bool:
        """Tests whether the formula's main connective is an implication"""
        return isinstance(self._formula, Implies)

    def is_bi_implication(self) -> bool:
        """Tests whether the formula's main connective is a bi-implication"""
        return isinstance(self._formula, BiImplies)

    def _eliminate_conditionals(self):
        return Formula(self._formula._eliminate_conditionals())

    def _move_negations_inward(self):
        return Formula(self._formula._move_negations_inward())

    def _distribute_or_over_and(self):
        return Formula(self._formula._distribute_or_over_and())

    def _distribute_and_over_or(self):
        return Formula(self._formula._distribute_and_over_or())

__init__(formula)

The formula's constructor

Parameters:

Name	Type	Description	Default
formula		the formula represented (can be an instance of any of the base connective classes)	required

Source code in src\logicalpy\core.py

def __init__(self, formula, /):
    """The formula's constructor

    Args:
        formula: the formula represented (can be an instance of any of the base connective classes)

    """
    self._formula = formula

from_string(formula_str) classmethod

Builds a formula from a string representation of it

Parameters:

Name	Type	Description	Default
formula_str	str	the string containing the string representation of the formula	required

Returns:

Type	Description
Formula	the formula built

Source code in src\logicalpy\core.py

@classmethod
def from_string(cls, formula_str: str):
    """Builds a formula from a string representation of it

    Args:
        formula_str (str): the string containing the string representation of the formula

    Returns:
        (Formula): the formula built

    """
    return cls(_interpret_formula_tree(PROPOSITIONAL_PARSER.parse(formula_str)))

is_bi_implication()

Tests whether the formula's main connective is a bi-implication

Source code in src\logicalpy\core.py

def is_bi_implication(self) -> bool:
    """Tests whether the formula's main connective is a bi-implication"""
    return isinstance(self._formula, BiImplies)

is_conjunction()

Tests whether the formula's main connective is a conjunction

Source code in src\logicalpy\core.py

def is_conjunction(self) -> bool:
    """Tests whether the formula's main connective is a conjunction"""
    return isinstance(self._formula, And)

is_disjunction()

Tests whether the formula's main connective is a disjunction

Source code in src\logicalpy\core.py

def is_disjunction(self) -> bool:
    """Tests whether the formula's main connective is a disjunction"""
    return isinstance(self._formula, Or)

is_implication()

Tests whether the formula's main connective is an implication

Source code in src\logicalpy\core.py

def is_implication(self) -> bool:
    """Tests whether the formula's main connective is an implication"""
    return isinstance(self._formula, Implies)

is_literal()

Tests whether the formula is a literal, i.e. a proposition or its negation

Source code in src\logicalpy\core.py

def is_literal(self) -> bool:
    """Tests whether the formula is a literal, i.e. a proposition or its negation"""
    if isinstance(self._formula, Proposition):
        return True
    elif isinstance(self._formula, Not):
        if isinstance(self._formula.a, Proposition):
            return True
    return False

is_negation()

Tests whether the formula's main connective is a negation

Source code in src\logicalpy\core.py

def is_negation(self) -> bool:
    """Tests whether the formula's main connective is a negation"""
    return isinstance(self._formula, Not)

is_proposition()

Tests whether the formula is only a proposition

Source code in src\logicalpy\core.py

def is_proposition(self) -> bool:
    """Tests whether the formula is only a proposition"""
    return isinstance(self._formula, Proposition)

is_satisfied(valuation)

Tests whether the formula is satisfied by the truth valuation given

Parameters:

Name	Type	Description	Default
valuation	dict[str, bool]	a dictionary associating each proposition name (str) with a truth value (bool)	required

Returns:

Type	Description
bool	True is the formula is satisfied by the truth valuation given, and False otherwise

Raises:

Type	Description
ValueError	if the truth value of one of the formula's propositions isn't precised in the valuation given

Source code in src\logicalpy\core.py

def is_satisfied(self, valuation: dict[str, bool]) -> bool:
    """Tests whether the formula is satisfied by the truth valuation given

    Args:
        valuation (dict[str, bool]): a dictionary associating each proposition name (str) with a truth value (bool)

    Returns:
        (bool): True is the formula is satisfied by the truth valuation given, and False otherwise

    Raises:
        ValueError: if the truth value of one of the formula's propositions isn't precised in the valuation given

    """
    return self._formula.is_satisfied(valuation)

propositions()

A method for listing all the propositions of the formula

Returns:

Type	Description
set[str]	the set of all the propositions of the formula, each represented by its name (str)

Source code in src\logicalpy\core.py

def propositions(self) -> set[str]:
    """A method for listing all the propositions of the formula

    Returns:
        (set[str]): the set of all the propositions of the formula, each represented by its name (str)

    """
    return self._formula.propositions()

to_latex()

Renders the formula as LaTeX code

Returns:

Type	Description
str	the LaTeX representation of the formula, as inline math

Source code in src\logicalpy\core.py

def to_latex(self) -> str:
    """Renders the formula as LaTeX code

    Returns:
        (str): the LaTeX representation of the formula, as inline math

    """
    formula_latex = self._formula.to_latex()
    if formula_latex.startswith("(") and formula_latex.endswith(
        ")"
    ):  # if there are outer parenthesis, we remove them
        return "$" + formula_latex[1:-1] + "$"
    return "$" + formula_latex + "$"

Implies

Bases: _TwoPlaceConnective

A class representing logical implication

Attributes:

Name	Type	Description
a		the left hand part of the implication
b		the right hand part of the implication

Source code in src\logicalpy\core.py

class Implies(_TwoPlaceConnective):
    """A class representing logical implication

    Attributes:
        a: the left hand part of the implication
        b: the right hand part of the implication
    """

    CONNECTIVE_SYMBOL = "→"
    LATEX_SYMBOL = r"\to"

    def is_satisfied(self, valuation: dict[str, bool]) -> bool:
        return (not self.a.is_satisfied(valuation)) or self.b.is_satisfied(valuation)

    def _eliminate_conditionals(self):
        return Or(
            Not(self.a._eliminate_conditionals()),
            self.b._eliminate_conditionals(),
        )

Not

A class representing logical negation

Attributes:

Name	Type	Description
a		the negated content

Source code in src\logicalpy\core.py

class Not:
    """A class representing logical negation

    Attributes:
        a: the negated content

    """

    def __init__(self, a, /):
        self.a = a

    def __str__(self) -> str:
        return f"¬{self.a}"

    def __eq__(self, other) -> bool:
        if isinstance(other, Not):
            return self.a == other.a
        return False

    def __repr__(self) -> str:
        return f"Not({repr(self.a)})"

    def to_latex(self) -> str:
        return r"\neg " + self.a.to_latex()

    def propositions(self) -> set[str]:
        return self.a.propositions()

    def is_satisfied(self, valuation: dict[str, bool]) -> bool:
        return not self.a.is_satisfied(valuation)

    def __and__(self, other):
        return And(self, other)

    def __or__(self, other):
        return Or(self, other)

    def __rshift__(self, other):
        return Implies(self, other)

    def __invert__(self):
        return Not(self)

    def _eliminate_conditionals(self):
        return Not(self.a._eliminate_conditionals())

    def _move_negations_inward(self):
        if isinstance(self.a, Not):  # double negation elimination
            return self.a.a._move_negations_inward()
        elif isinstance(self.a, And):  # De Morgan's law #1 (~(A & B) <-> ~A v ~B)
            return Or(
                Not(self.a.a)._move_negations_inward(),
                Not(self.a.b)._move_negations_inward(),
            )
        elif isinstance(self.a, Or):  # De Morgan's law #2 (~(A v B) <-> ~A & ~B)
            return And(
                Not(self.a.a)._move_negations_inward(),
                Not(self.a.b)._move_negations_inward(),
            )
        else:  # matches no rule
            return self

    def _distribute_or_over_and(self):
        return Not(self.a._distribute_or_over_and())

    def _distribute_and_over_or(self):
        return Not(self.a._distribute_and_over_or())

Or

Bases: _TwoPlaceConnective

A class representing logical disjunction

Attributes:

Name	Type	Description
a		the left hand part of the disjunction
b		the right hand part of the disjunction

Source code in src\logicalpy\core.py

class Or(_TwoPlaceConnective):
    """A class representing logical disjunction

    Attributes:
        a: the left hand part of the disjunction
        b: the right hand part of the disjunction
    """

    CONNECTIVE_SYMBOL = "∨"
    LATEX_SYMBOL = r"\lor"

    def is_satisfied(self, valuation: dict[str, bool]) -> bool:
        return self.a.is_satisfied(valuation) or self.b.is_satisfied(valuation)

    def _distribute_or_over_and(self):
        if isinstance(self.b, And):
            return And(
                Or(self.a, self.b.a)._distribute_or_over_and(),
                Or(self.a, self.b.b)._distribute_or_over_and(),
            )
        elif isinstance(self.a, And):
            return And(
                Or(self.b, self.a.a)._distribute_or_over_and(),
                Or(self.b, self.a.b)._distribute_or_over_and(),
            )
        else:
            return Or(
                self.a._distribute_or_over_and(),
                self.b._distribute_or_over_and(),
            )

Proposition

A class representing propositions

Attributes:

Name	Type	Description
name	str	the name of the proposition

Source code in src\logicalpy\core.py

class Proposition:
    """A class representing propositions

    Attributes:
        name (str): the name of the proposition
    """

    def __init__(self, name: str):
        if name.strip() == "":
            raise ValueError("proposition name cannot be empty")
        self.name = name

    def __str__(self) -> str:
        return self.name

    def __eq__(self, other):
        if isinstance(other, Proposition):
            return self.name == other.name
        return False

    def __repr__(self) -> str:
        return f"Proposition('{self.name}')"

    def to_latex(self) -> str:
        return self.name

    def propositions(self) -> set:
        return {self.name}

    def is_satisfied(self, valuation: dict[str, bool]) -> bool:
        try:
            return valuation[self.name]
        except KeyError:
            raise ValueError(
                f"proposition '{self.name}' is not associated with a value"
            )

    def __and__(self, other):
        return And(self, other)

    def __or__(self, other):
        return Or(self, other)

    def __rshift__(self, other):
        return Implies(self, other)

    def __invert__(self):
        return Not(self)

    def _eliminate_conditionals(self):
        return self

    def _move_negations_inward(self):
        return self

    def _distribute_or_over_and(self):
        return self

    def _distribute_and_over_or(self):
        return self