diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index e7dbe6a..6953014 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -27,11 +27,23 @@ jobs: - name: Install dependencies run: | python -m pip install --upgrade pip - python -m pip install flake8 mypy + python -m pip install flake8 mypy pylint if [ -f requirements.txt ]; then pip install -r requirements.txt; fi - name: Lint with flake8 run: | flake8 ./tests/*.py ./logic/*.py --max-line-length=120 + - name: Lint with pylint + continue-on-error: true + run: | + pylint ./tests/*.py ./logic/*.py --max-line-length=120 --disable W1114 --disable C0103 + # W1114: arguments-out-of-order (pylint getting confused) + # C0103: invalid-name + # R0914: too-many-locals + # R0911: too-many-return-statements + # R0912: too-many-branches + # R0915: too-many-statements + # R0903: too-few-public-methods + - name: Type checker with mypy run: | mypy ./tests/*.py ./logic/*.py diff --git a/logic/__init__.py b/logic/__init__.py index 2894d76..2c08bed 100644 --- a/logic/__init__.py +++ b/logic/__init__.py @@ -1,4 +1,6 @@ -from .proof import Prover, Proof -from .proposition import Proposition, IMPLY, IFF, AND, OR, NOT +"""Logic is a predicate logic simulator and a automated prover""" + +from .proof import Proof, Prover +from .proposition import AND, IFF, IMPLY, NOT, OR, Proposition __all__ = ["Proposition", "Proof", "Prover", "IMPLY", "IFF", "AND", "OR", "NOT"] diff --git a/logic/proof.py b/logic/proof.py index 644eb8f..22eaeb8 100644 --- a/logic/proof.py +++ b/logic/proof.py @@ -1,28 +1,30 @@ -from typing import Sequence, Generator, Iterator, TypeAlias, Any +"""All functions and classes related to construction of +proofs, assumptions and Prover to automated proving""" + +from enum import Enum +from typing import Any, Generator, Iterator, Sequence, TypeAlias, Union + from .proposition import ( - Statement, + IMPLY, CompositePropositionAND, - CompositePropositionNOT, - CompositePropositionOR, CompositePropositionBICONDITIONAL, CompositePropositionCONDITIONAL, - IMPLY, + CompositePropositionNOT, + CompositePropositionOR, + Statement, ) -from enum import Enum - AssumptionT: TypeAlias = "Assumption" ProofT: TypeAlias = "Proof" - - -class ProofStrategy(Enum): - pass +ProofStrategy: TypeAlias = Union["Equivalence", "RulesOfInference"] ProofEntryT = tuple[Statement, ProofStrategy, tuple[Statement, ...]] -class Equivalence(ProofStrategy): +class Equivalence(Enum): + """Enum to represent all type of equivalences""" + DefinitionOfBiConditional = "Definition Of Bi-Conditional" DeMorgensLaw = "De'Morgen's Law" NotOfNot = "Not Of Not" @@ -32,7 +34,9 @@ def __str__(self) -> str: return self.value -class RulesOfInference(ProofStrategy): +class RulesOfInference(Enum): + """Enum of all Rules Of Inference which can be used to construct proofs""" + ModusPonens = "Modus Ponens" ModusTollens = "Modus Tollens" HypotheticalSyllogism = "Hypothetical Syllogism" @@ -47,7 +51,17 @@ def __str__(self) -> str: class Assumption: - def __init__(self, assumptions: Sequence[Statement] | set[Statement] | AssumptionT) -> None: + """Class to hold and operate on all assumptions used in a proof""" + + def __init__( + self, assumptions: Sequence[Statement] | set[Statement] | AssumptionT + ) -> None: + """Constructs Assumption + + Args: + assumptions (Sequence[Statement] | set[Statement] | AssumptionT): Sequence + or set of Statements + """ if isinstance(assumptions, Assumption): self.assumptions: set[Statement] = set(assumptions.assumptions) else: @@ -59,11 +73,24 @@ def __contains__(self, key: Any) -> bool: def __str__(self) -> str: result = "" for i in self.assumptions: - result += "{:>28}\n".format(str(i)) + result += f"{str(i):>28}\n" return result - def with_proposition(self, prop: Statement) -> Generator[Statement, None, None]: - individual_propositions = prop.extract() + def with_proposition( + self, statement: Statement + ) -> Generator[Statement, None, None]: + """ + Returns a generator of all assumptions with contain at least one proposition + from statement + + Args: + statement (Statement): Proportions to look for + + Yields: + Generator[Statement, None, None]: Assumptions that contain the given + proposition + """ + individual_propositions = statement.extract() for i in self.assumptions: yielded = False for j in individual_propositions: @@ -71,24 +98,63 @@ def with_proposition(self, prop: Statement) -> Generator[Statement, None, None]: yielded = True yield i - if not yielded and prop in i: + if not yielded and statement in i: yield i - def remove(self, *statement: Statement) -> AssumptionT: - return Assumption(self.assumptions - {*statement}) + def remove(self, *statements: Statement) -> AssumptionT: + """ + Constructs and returns new Assumption that does not contain any of the given + statements. statements can be 1 or more Statement. + + Returns: + Assumption: Returns newly constructed Assumption + """ + return Assumption(self.assumptions - {*statements}) def add(self, *statement: Statement) -> AssumptionT: + """ + Constructs and returns new Assumption that with all of the given statements. + statements can be 1 or more Statement. + + Returns: + Assumption: Returns newly constructed Assumption + """ return Assumption(self.assumptions.union({*statement})) class Proof: + """Class to create, operate and verify on a proof""" + def __init__(self, proof: list[ProofEntryT] | None = None) -> None: + """Constructs Proof object + + Args: + proof (list[tuple[Statement, ProofStrategy, *Statement]] | None, optional): + List of triple tuple + (Conclusion, Rule of Inference or Equivalence use, Assumptions used). + Defaults to None. + """ self.proof: list[ProofEntryT] = proof if proof else [] - def add_step(self, conclusion: Statement, roi: ProofStrategy, *statement: Statement) -> None: - self.proof.append((conclusion, roi, (*statement,))) + def add_step( + self, conclusion: Statement, strategy: ProofStrategy, *statements: Statement + ) -> None: + """Adds a new step to the proof + + Args: + conclusion (Statement): Conclusion that is derived in this step + strategy (ProofStrategy): The Equivalence or Rule of Inference + used in this step + statements (Statement): 1 or more statements used in this step + """ + self.proof.append((conclusion, strategy, (*statements,))) def extend(self, proof: ProofT) -> None: + """extend this proof with another proof + + Args: + proof (ProofT): Another proof to extend this proof with + """ self.proof.extend(proof.proof) def __iter__(self) -> Iterator[ProofEntryT]: @@ -97,18 +163,26 @@ def __iter__(self) -> Iterator[ProofEntryT]: def __str__(self) -> str: result = "" for conclusion, rof, statements in self: - result += "{:>28} {:>28} {:28}\n".format( - str(conclusion), str(rof), "{" + ", ".join(str(i) for i in statements) + "}" - ) + statements_string = "{" + ", ".join(str(i) for i in statements) + "}" + result += f"{str(conclusion):>28} {str(rof):>28} {statements_string:28}\n" return result class Prover: + """Class used for the automated proving""" + def __init__( self, assumptions: Sequence[Statement] | Assumption, conclusion: Statement, ) -> None: + """Constructs Prover class + + Args: + assumptions (Sequence[Statement] | Assumption): Assumptions to be used in + the proof + conclusion (Statement): Conclusion that we want to prove + """ if isinstance(assumptions, Assumption): self.assumptions = assumptions else: @@ -124,47 +198,84 @@ def _prove_decomposed_conclusion(self) -> tuple[Proof, bool]: proof, truth = Prover(self.assumptions, statement.statement).prove() if truth: self.proof.extend(proof) - self.proof.add_step(self.conclusion, Equivalence.NotOfNot, statement.statement) + self.proof.add_step( + self.conclusion, Equivalence.NotOfNot, statement.statement + ) return self.proof, True # Applying De'Morgen's Law match statement: case CompositePropositionAND(first=first, second=second): - proof, truth = Prover(self.assumptions, ~first | ~second).prove() + proof, truth = Prover( + self.assumptions, ~first | ~second + ).prove() if truth: self.proof.extend(proof) - self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, ~first | ~second) + self.proof.add_step( + self.conclusion, + Equivalence.DeMorgensLaw, + ~first | ~second, + ) return self.proof, True case CompositePropositionOR(first=first, second=second): - proof, truth = Prover(self.assumptions, ~first & ~second).prove() + proof, truth = Prover( + self.assumptions, ~first & ~second + ).prove() if truth: self.proof.extend(proof) - self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, ~first & ~second) + self.proof.add_step( + self.conclusion, + Equivalence.DeMorgensLaw, + ~first & ~second, + ) return self.proof, True case CompositePropositionOR(first=first, second=second): # Applying x | ~x <-> True if first == ~second or ~first == second: - return Proof([(self.conclusion, Equivalence.Complement, (self.conclusion,))]), True + return ( + Proof( + [ + ( + self.conclusion, + Equivalence.Complement, + (self.conclusion,), + ) + ] + ), + True, + ) # Applying Addition - proof_first, truth_first = Prover(self.assumptions.remove(self.conclusion), first).prove() + proof_first, truth_first = Prover( + self.assumptions.remove(self.conclusion), first + ).prove() if truth_first: self.proof.extend(proof_first) - self.proof.add_step(self.conclusion, RulesOfInference.Addition, first, second) + self.proof.add_step( + self.conclusion, RulesOfInference.Addition, first, second + ) return self.proof, True - proof_second, truth_second = Prover(self.assumptions.remove(self.conclusion), second).prove() + proof_second, truth_second = Prover( + self.assumptions.remove(self.conclusion), second + ).prove() if truth_second: self.proof.extend(proof_second) - self.proof.add_step(self.conclusion, RulesOfInference.Addition, second, first) + self.proof.add_step( + self.conclusion, RulesOfInference.Addition, second, first + ) return self.proof, True # Applying De'Morgen's Law - if isinstance(first, CompositePropositionNOT) and isinstance(second, CompositePropositionNOT): + if isinstance(first, CompositePropositionNOT) and isinstance( + second, CompositePropositionNOT + ): proof, truth = Prover(self.assumptions, ~(first & second)).prove() if truth: self.proof.extend(proof) - self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, ~(first & second)) + self.proof.add_step( + self.conclusion, Equivalence.DeMorgensLaw, ~(first & second) + ) return self.proof, True case CompositePropositionAND(first=first, second=second): @@ -173,30 +284,44 @@ def _prove_decomposed_conclusion(self) -> tuple[Proof, bool]: return Proof(), False # Applying Conjunction - proof_first, truth_first = Prover(self.assumptions.remove(self.conclusion), first).prove() - proof_second, truth_second = Prover(self.assumptions.remove(self.conclusion), second).prove() + proof_first, truth_first = Prover( + self.assumptions.remove(self.conclusion), first + ).prove() + proof_second, truth_second = Prover( + self.assumptions.remove(self.conclusion), second + ).prove() if truth_first and truth_second: self.proof.extend(proof_first) self.proof.extend(proof_second) - self.proof.add_step(self.conclusion, RulesOfInference.Conjunction, first, second) + self.proof.add_step( + self.conclusion, RulesOfInference.Conjunction, first, second + ) return self.proof, True # Applying De'Morgen's Law - if isinstance(first, CompositePropositionNOT) and isinstance(second, CompositePropositionNOT): + if isinstance(first, CompositePropositionNOT) and isinstance( + second, CompositePropositionNOT + ): proof, truth = Prover(self.assumptions, ~(first | second)).prove() if truth: self.proof.extend(proof) - self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, ~(first | second)) + self.proof.add_step( + self.conclusion, Equivalence.DeMorgensLaw, ~(first | second) + ) return self.proof, True - case CompositePropositionBICONDITIONAL(assumption=assumption, conclusion=conclusion): + case CompositePropositionBICONDITIONAL( + assumption=assumption, conclusion=conclusion + ): # Applying definition of Bi-Conditional # (p <-> q) -> (p -> q) & (q -> p) proof_p_implies_q, truth_p_implies_q = Prover( - self.assumptions.remove(self.conclusion), IMPLY(assumption, conclusion) + self.assumptions.remove(self.conclusion), + IMPLY(assumption, conclusion), ).prove() proof_q_implies_p, truth_q_implies_p = Prover( - self.assumptions.remove(self.conclusion), IMPLY(conclusion, assumption) + self.assumptions.remove(self.conclusion), + IMPLY(conclusion, assumption), ).prove() if truth_p_implies_q and truth_q_implies_p: self.proof.extend(proof_p_implies_q) @@ -212,6 +337,13 @@ def _prove_decomposed_conclusion(self) -> tuple[Proof, bool]: return Proof(), False def prove(self) -> tuple[Proof, bool]: + """Tries to prove the given conclusion with the given assumptions + + Returns: + tuple[Proof, bool]: Proof to prove the conclusion if conclusion is true + otherwise an empty Proof, True if the conclusion was proved + otherwise False + """ if self.conclusion in self.assumptions: return self.proof, True @@ -221,151 +353,244 @@ def prove(self) -> tuple[Proof, bool]: # Applying NotOfNot i.e. ~(~x) <-> x if isinstance(statement, CompositePropositionNOT): if statement.statement != self.conclusion: - if not (statement.statement in self.assumptions): + if statement.statement not in self.assumptions: proof, truth = Prover( - self.assumptions.add(statement.statement), self.conclusion + self.assumptions.add(statement.statement), + self.conclusion, ).prove() if truth: - self.proof.add_step(self.conclusion, Equivalence.NotOfNot, i) + self.proof.add_step( + self.conclusion, Equivalence.NotOfNot, i + ) self.proof.extend(proof) return self.proof, True else: - self.proof.add_step(self.conclusion, Equivalence.NotOfNot, i) + self.proof.add_step( + self.conclusion, Equivalence.NotOfNot, i + ) return self.proof, True # Applying De'Morgan's Law match statement: case CompositePropositionAND(first=first, second=second): if (~first | ~second) != self.conclusion: - if not ((~first | ~second) in self.assumptions): + if (~first | ~second) not in self.assumptions: proof, truth = Prover( - self.assumptions.add(~first | ~second), self.conclusion + self.assumptions.add(~first | ~second), + self.conclusion, ).prove() if truth: - self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, i) + self.proof.add_step( + self.conclusion, Equivalence.DeMorgensLaw, i + ) self.proof.extend(proof) return proof, True else: - self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, i) + self.proof.add_step( + self.conclusion, Equivalence.DeMorgensLaw, i + ) return self.proof, True case CompositePropositionOR(first=first, second=second): if ~first & ~second != self.conclusion: - if not ((~first & ~second) in self.assumptions): + if (~first & ~second) not in self.assumptions: proof, truth = Prover( - self.assumptions.add(~first & ~second), self.conclusion + self.assumptions.add(~first & ~second), + self.conclusion, ).prove() if truth: - self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, i) + self.proof.add_step( + self.conclusion, Equivalence.DeMorgensLaw, i + ) self.proof.extend(proof) return self.proof, True else: - self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, i) + self.proof.add_step( + self.conclusion, Equivalence.DeMorgensLaw, i + ) return self.proof, True case CompositePropositionOR(first=first, second=second): # Applying Resolution if isinstance(self.conclusion, CompositePropositionOR): if self.conclusion.first == first: - proof, truth = Prover(self.assumptions.remove(i), ~second | self.conclusion.second).prove() + proof, truth = Prover( + self.assumptions.remove(i), + ~second | self.conclusion.second, + ).prove() self.proof.extend(proof) self.proof.add_step( - self.conclusion, RulesOfInference.Resolution, i, ~second | self.conclusion.second + self.conclusion, + RulesOfInference.Resolution, + i, + ~second | self.conclusion.second, ) return self.proof, True if self.conclusion.second == second: - proof, truth = Prover(self.assumptions.remove(i), ~first | self.conclusion.first).prove() + proof, truth = Prover( + self.assumptions.remove(i), + ~first | self.conclusion.first, + ).prove() self.proof.extend(proof) self.proof.add_step( - self.conclusion, RulesOfInference.Resolution, i, ~first | self.conclusion.first + self.conclusion, + RulesOfInference.Resolution, + i, + ~first | self.conclusion.first, ) return self.proof, True if self.conclusion.first == second: - proof, truth = Prover(self.assumptions.remove(i), ~first | self.conclusion.second).prove() + proof, truth = Prover( + self.assumptions.remove(i), + ~first | self.conclusion.second, + ).prove() self.proof.extend(proof) self.proof.add_step( - self.conclusion, RulesOfInference.Resolution, i, ~first | self.conclusion.second + self.conclusion, + RulesOfInference.Resolution, + i, + ~first | self.conclusion.second, ) return self.proof, True if self.conclusion.second == first: - proof, truth = Prover(self.assumptions.remove(i), ~second | self.conclusion.first).prove() + proof, truth = Prover( + self.assumptions.remove(i), + ~second | self.conclusion.first, + ).prove() self.proof.extend(proof) self.proof.add_step( - self.conclusion, RulesOfInference.Resolution, i, ~second | self.conclusion.first + self.conclusion, + RulesOfInference.Resolution, + i, + ~second | self.conclusion.first, ) return self.proof, True # Applying Disjunctive Syllogism if self.conclusion == first: - proof, truth = Prover(self.assumptions.remove(i), ~second).prove() + proof, truth = Prover( + self.assumptions.remove(i), ~second + ).prove() if truth: self.proof.extend(proof) - self.proof.add_step(self.conclusion, RulesOfInference.DisjunctiveSyllogism, i, ~second) + self.proof.add_step( + self.conclusion, + RulesOfInference.DisjunctiveSyllogism, + i, + ~second, + ) return self.proof, True if self.conclusion == second: - proof, truth = Prover(self.assumptions.remove(i), ~first).prove() + proof, truth = Prover( + self.assumptions.remove(i), ~first + ).prove() if truth: self.proof.extend(proof) - self.proof.add_step(self.conclusion, RulesOfInference.DisjunctiveSyllogism, i, ~first) + self.proof.add_step( + self.conclusion, + RulesOfInference.DisjunctiveSyllogism, + i, + ~first, + ) return self.proof, True # Applying De'Morgen's Law - if isinstance(first, CompositePropositionNOT) and isinstance(second, CompositePropositionNOT): + if isinstance(first, CompositePropositionNOT) and isinstance( + second, CompositePropositionNOT + ): if ~(first.statement & second.statement) != self.conclusion: - if not (~(first.statement & second.statement) in self.assumptions): + if not ( + ~(first.statement & second.statement) + in self.assumptions + ): proof, truth = Prover( - self.assumptions.add(~(first.statement & second.statement)), self.conclusion + self.assumptions.add( + ~(first.statement & second.statement) + ), + self.conclusion, ).prove() if truth: - self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, i) + self.proof.add_step( + self.conclusion, Equivalence.DeMorgensLaw, i + ) self.proof.extend(proof) return self.proof, True else: - self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, i) + self.proof.add_step( + self.conclusion, Equivalence.DeMorgensLaw, i + ) return self.proof, True case CompositePropositionAND(first=first, second=second): # Applying De'Morgen's Law - if isinstance(first, CompositePropositionNOT) and isinstance(second, CompositePropositionNOT): + if isinstance(first, CompositePropositionNOT) and isinstance( + second, CompositePropositionNOT + ): if ~(first.statement | second.statement) != self.conclusion: - if not (~(first.statement | second.statement) in self.assumptions): + if not ( + ~(first.statement | second.statement) + in self.assumptions + ): proof, truth = Prover( - self.assumptions.add(~(first.statement | second.statement)), self.conclusion + self.assumptions.add( + ~(first.statement | second.statement) + ), + self.conclusion, ).prove() if truth: - self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, i) + self.proof.add_step( + self.conclusion, Equivalence.DeMorgensLaw, i + ) self.proof.extend(proof) return self.proof, True else: - self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, i) + self.proof.add_step( + self.conclusion, Equivalence.DeMorgensLaw, i + ) return self.proof, True # Applying Simplification - if first != self.conclusion and second != self.conclusion: - if not (first in self.assumptions) or not (second in self.assumptions): - proof, truth = Prover(self.assumptions.add(first, second), self.conclusion).prove() + if self.conclusion not in (first, second): + if ( + first not in self.assumptions + or second not in self.assumptions + ): + proof, truth = Prover( + self.assumptions.add(first, second), self.conclusion + ).prove() if truth: - self.proof.add_step(self.conclusion, RulesOfInference.Simplification, i) + self.proof.add_step( + self.conclusion, RulesOfInference.Simplification, i + ) self.proof.extend(proof) return self.proof, True else: - self.proof.add_step(self.conclusion, RulesOfInference.Simplification, i) + self.proof.add_step( + self.conclusion, RulesOfInference.Simplification, i + ) return self.proof, True - case CompositePropositionCONDITIONAL(assumption=assumption, conclusion=conclusion): + case CompositePropositionCONDITIONAL( + assumption=assumption, conclusion=conclusion + ): # Applying Modus Ponens if ( - (not (conclusion in self.assumptions)) + conclusion not in self.assumptions and self.conclusion != assumption and self.conclusion != ~conclusion ): - proof, truth = Prover(self.assumptions.remove(i), assumption).prove() + proof, truth = Prover( + self.assumptions.remove(i), assumption + ).prove() if truth: self.proof.extend(proof) - self.proof.add_step(conclusion, RulesOfInference.ModusPonens, i, assumption) + self.proof.add_step( + conclusion, RulesOfInference.ModusPonens, i, assumption + ) if self.conclusion != conclusion: proof, truth = Prover( - self.assumptions.remove(i).add(conclusion), self.conclusion + self.assumptions.remove(i).add(conclusion), + self.conclusion, ).prove() if truth: self.proof.extend(proof) @@ -375,17 +600,25 @@ def prove(self) -> tuple[Proof, bool]: # Applying Modus Tollens if ( - (not (~assumption in self.assumptions)) + ~assumption not in self.assumptions and self.conclusion != ~conclusion and self.conclusion != assumption ): - proof, truth = Prover(self.assumptions.remove(i), ~conclusion).prove() + proof, truth = Prover( + self.assumptions.remove(i), ~conclusion + ).prove() if truth: self.proof.extend(proof) - self.proof.add_step(~assumption, RulesOfInference.ModusTollens, i, ~conclusion) + self.proof.add_step( + ~assumption, + RulesOfInference.ModusTollens, + i, + ~conclusion, + ) if self.conclusion != ~assumption: proof, truth = Prover( - self.assumptions.remove(i).add(~assumption), self.conclusion + self.assumptions.remove(i).add(~assumption), + self.conclusion, ).prove() if truth: self.proof.extend(proof) @@ -410,27 +643,37 @@ def prove(self) -> tuple[Proof, bool]: ) return self.proof, True - case CompositePropositionBICONDITIONAL(assumption=assumption, conclusion=conclusion): + case CompositePropositionBICONDITIONAL( + assumption=assumption, conclusion=conclusion + ): # Applying definition of Bi-Conditional # (p <-> q) -> (p -> q) & (q -> p) if ( IMPLY(assumption, conclusion) == self.conclusion or IMPLY(conclusion, assumption) == self.conclusion ): - self.proof.add_step(self.conclusion, Equivalence.DefinitionOfBiConditional, i) + self.proof.add_step( + self.conclusion, Equivalence.DefinitionOfBiConditional, i + ) return self.proof, True - if (not (IMPLY(assumption, conclusion) in self.assumptions)) or ( - not (IMPLY(conclusion, assumption) in self.assumptions) + if ( + IMPLY(assumption, conclusion) not in self.assumptions + or IMPLY(conclusion, assumption) not in self.assumptions ): proof, truth = Prover( self.assumptions.remove(i).add( - IMPLY(conclusion, assumption), IMPLY(assumption, conclusion) + IMPLY(conclusion, assumption), + IMPLY(assumption, conclusion), ), self.conclusion, ).prove() if truth: - self.proof.add_step(self.conclusion, Equivalence.DefinitionOfBiConditional, i) + self.proof.add_step( + self.conclusion, + Equivalence.DefinitionOfBiConditional, + i, + ) self.proof.extend(proof) return self.proof, True diff --git a/logic/proposition.py b/logic/proposition.py index 16e9e4f..4963844 100644 --- a/logic/proposition.py +++ b/logic/proposition.py @@ -1,7 +1,10 @@ -from typing import Any, TypeAlias +"""All functions and classes related to creation of propositions +and operation between propositions""" + from abc import ABC, abstractmethod -from warnings import warn from dataclasses import dataclass +from typing import Any, TypeAlias +from warnings import warn PropositionT: TypeAlias = "Proposition" CompositePropositionT: TypeAlias = "CompositeProposition" @@ -10,17 +13,32 @@ @dataclass(frozen=True) class Statement(ABC): + """Base class to represent any type of proposition""" + @abstractmethod def remove_conditionals(self) -> StatementT: - pass + """Remove all conditions and change it to boolean logic. + Example: p -> q to ~p | q + + Returns: + StatementT: Statement without any conditions or bi-conditionals + """ @abstractmethod def simplify(self) -> StatementT: - pass + """Simplifies the given statement + + Returns: + StatementT: Simplified statement + """ @abstractmethod def extract(self) -> list[PropositionT]: - pass + """Extracts individual propositions used in this statement + + Returns: + list[PropositionT]: List of all individual Propositions + """ @abstractmethod def __contains__(self, key: Any) -> bool: @@ -28,12 +46,16 @@ def __contains__(self, key: Any) -> bool: def __and__(self, other: Any) -> StatementT: if not isinstance(other, Statement): - raise TypeError(f"Cannot perform logical and of {type(self)} with {type(other)}") + raise TypeError( + f"Cannot perform logical and of {type(self)} with {type(other)}" + ) return CompositePropositionAND(self, other) def __or__(self, other: Any) -> StatementT: if not isinstance(other, Statement): - raise TypeError(f"Cannot perform logical or of {type(self)} with {type(other)}") + raise TypeError( + f"Cannot perform logical or of {type(self)} with {type(other)}" + ) return CompositePropositionOR(self, other) def __invert__(self) -> StatementT: @@ -42,6 +64,8 @@ def __invert__(self) -> StatementT: @dataclass(frozen=True) class Proposition(Statement): + """Representation of a Proposition""" + variable: str statement: str = "" @@ -59,7 +83,9 @@ def __str__(self) -> str: def __contains__(self, key: Any) -> bool: if not isinstance(key, Statement): - raise TypeError(f"Cannot perform in operation of {type(self)} with {type(key)}") + raise TypeError( + f"Cannot perform in operation of {type(self)} with {type(key)}" + ) if isinstance(key, Proposition): return self == key @@ -78,6 +104,8 @@ def __eq__(self, other: Any) -> bool: @dataclass(frozen=True) class CompositeProposition(Statement): + """Representation of a Proposition constructed with some operator""" + def simplify(self) -> StatementT: warn("Not Implemented") return self @@ -85,11 +113,15 @@ def simplify(self) -> StatementT: @dataclass(frozen=True) class CompositePropositionAND(CompositeProposition): + """Representation of p & q""" + first: Statement second: Statement def remove_conditionals(self) -> StatementT: - return CompositePropositionAND(self.first.remove_conditionals(), self.second.remove_conditionals()) + return CompositePropositionAND( + self.first.remove_conditionals(), self.second.remove_conditionals() + ) def extract(self) -> list[PropositionT]: return [*self.first.extract(), *self.second.extract()] @@ -99,7 +131,9 @@ def __str__(self) -> str: def __contains__(self, key: Any) -> bool: if not isinstance(key, Statement): - raise TypeError(f"Cannot perform in operation of {type(self)} with {type(key)}") + raise TypeError( + f"Cannot perform in operation of {type(self)} with {type(key)}" + ) return key in self.first or key in self.second or key == self @@ -117,11 +151,15 @@ def __eq__(self, other: Any) -> bool: @dataclass(frozen=True) class CompositePropositionOR(CompositeProposition): + """Representation of p | q""" + first: Statement second: Statement def remove_conditionals(self) -> StatementT: - return CompositePropositionOR(self.first.remove_conditionals(), self.second.remove_conditionals()) + return CompositePropositionOR( + self.first.remove_conditionals(), self.second.remove_conditionals() + ) def extract(self) -> list[PropositionT]: return [*self.first.extract(), *self.second.extract()] @@ -131,7 +169,9 @@ def __str__(self) -> str: def __contains__(self, key: Any) -> bool: if not isinstance(key, Statement): - raise TypeError(f"Cannot perform in operation of {type(self)} with {type(key)}") + raise TypeError( + f"Cannot perform in operation of {type(self)} with {type(key)}" + ) return key in self.first or key in self.second or key == self @@ -149,6 +189,8 @@ def __eq__(self, other: Any) -> bool: @dataclass(frozen=True) class CompositePropositionNOT(CompositeProposition): + """Representation of ~p""" + statement: Statement def remove_conditionals(self) -> StatementT: @@ -162,7 +204,9 @@ def __str__(self) -> str: def __contains__(self, key: Any) -> bool: if not isinstance(key, Statement): - raise TypeError(f"Cannot perform in operation of {type(self)} with {type(key)}") + raise TypeError( + f"Cannot perform in operation of {type(self)} with {type(key)}" + ) return key in self.statement or key == self @@ -171,8 +215,6 @@ def __eq__(self, other: Any) -> bool: raise TypeError(f"Cannot compare {type(self)} with {type(other)}") if isinstance(other, CompositePropositionNOT): - # FIXME: this should be part of the proof - # By Equivalence of ~(~x) <-> x return self.statement == other.statement return False @@ -180,11 +222,16 @@ def __eq__(self, other: Any) -> bool: @dataclass(frozen=True) class CompositePropositionCONDITIONAL(CompositeProposition): + """Representation of p -> q""" + assumption: Statement conclusion: Statement def remove_conditionals(self) -> StatementT: - return ~self.assumption.remove_conditionals() | self.conclusion.remove_conditionals() + return ( + ~self.assumption.remove_conditionals() + | self.conclusion.remove_conditionals() + ) def extract(self) -> list[PropositionT]: return [*self.assumption.extract(), *self.conclusion.extract()] @@ -194,7 +241,9 @@ def __str__(self) -> str: def __contains__(self, key: Any) -> bool: if not isinstance(key, Statement): - raise TypeError(f"Cannot perform in operation of {type(self)} with {type(key)}") + raise TypeError( + f"Cannot perform in operation of {type(self)} with {type(key)}" + ) return ( key in self.assumption @@ -209,13 +258,18 @@ def __eq__(self, other: Any) -> bool: raise TypeError(f"Cannot compare {type(self)} with {type(other)}") if isinstance(other, CompositePropositionCONDITIONAL): - return self.assumption == other.assumption and self.conclusion == other.conclusion + return ( + self.assumption == other.assumption + and self.conclusion == other.conclusion + ) return False @dataclass(frozen=True) class CompositePropositionBICONDITIONAL(CompositeProposition): + """Representation of p <-> q""" + assumption: Statement conclusion: Statement @@ -232,7 +286,9 @@ def __str__(self) -> str: def __contains__(self, key: Any) -> bool: if not isinstance(key, Statement): - raise TypeError(f"Cannot perform in operation of {type(self)} with {type(key)}") + raise TypeError( + f"Cannot perform in operation of {type(self)} with {type(key)}" + ) return ( key in self.assumption @@ -247,19 +303,46 @@ def __eq__(self, other: Any) -> bool: raise TypeError(f"Cannot compare {type(self)} with {type(other)}") if isinstance(other, CompositePropositionBICONDITIONAL): - return self.assumption == other.assumption and self.conclusion == other.conclusion + return ( + self.assumption == other.assumption + and self.conclusion == other.conclusion + ) return False -def AND(first: Statement, second: Statement, *others: Statement) -> CompositePropositionAND: +def AND( + first: Statement, second: Statement, *others: Statement +) -> CompositePropositionAND: + """Constructs Composite Proportions with & as the operators between them + + Args: + first (Statement): First proposition + second (Statement): Second proposition + others (*Statement): Any length of other propositions + + Returns: + CompositePropositionAND: Proposition and(ed) with all given propositions + """ if len(others) == 0: return CompositePropositionAND(first, second) return CompositePropositionAND(first, AND(second, *others)) -def OR(first: Statement, second: Statement, *others: Statement) -> CompositePropositionOR: +def OR( + first: Statement, second: Statement, *others: Statement +) -> CompositePropositionOR: + """Constructs Composite Proportions with | as the operators between them + + Args: + first (Statement): First proposition + second (Statement): Second proposition + others (*Statement): Any length of other propositions + + Returns: + CompositePropositionAND: Proposition or(ed) with all given propositions + """ if len(others) == 0: return CompositePropositionOR(first, second) @@ -267,12 +350,43 @@ def OR(first: Statement, second: Statement, *others: Statement) -> CompositeProp def NOT(statement: Statement) -> CompositePropositionNOT: + """Constructs Composite Proposition that is ~ of statement + + Args: + statement (Statement): Proposition to negate + + Returns: + CompositePropositionNOT: Negated Proposition + """ return CompositePropositionNOT(statement) -def IMPLY(assumption: Statement, conclusion: Statement) -> CompositePropositionCONDITIONAL: +def IMPLY( + assumption: Statement, conclusion: Statement +) -> CompositePropositionCONDITIONAL: + """Construct Composite Proposition with -> as the operator between them + + Args: + assumption (Statement): The assumption proposition + conclusion (Statement): The conclusion proposition + + Returns: + CompositePropositionCONDITIONAL: Conditional Proposition + """ return CompositePropositionCONDITIONAL(assumption, conclusion) -def IFF(assumption: Statement, conclusion: Statement) -> CompositePropositionBICONDITIONAL: +def IFF( + assumption: Statement, conclusion: Statement +) -> CompositePropositionBICONDITIONAL: + """Construct Composite Proposition with <-> as the operator between them. + i.e. constructs if and only if + + Args: + assumption (Statement): The assumption proposition + conclusion (Statement): The conclusion proposition + + Returns: + CompositePropositionBICONDITIONAL: Bi-Conditional Proposition + """ return CompositePropositionBICONDITIONAL(assumption, conclusion) diff --git a/tests/test_prover.py b/tests/test_prover.py index e85fc29..4b7057e 100644 --- a/tests/test_prover.py +++ b/tests/test_prover.py @@ -1,3 +1,5 @@ +"""Tests for the Prover class""" + import unittest from logic import Proposition, Prover, IMPLY, IFF @@ -5,6 +7,8 @@ class TestProver(unittest.TestCase): + """Tests for the Prover class""" + def setUp(self) -> None: self.x = Proposition("x") self.y = Proposition("y") @@ -14,6 +18,7 @@ def setUp(self) -> None: self.r = Proposition("r") def test_prover_modus_ponens(self): + """Tests the Modus Ponens rule of inference""" assumptions = ( self.p, IMPLY(self.p, self.q), @@ -27,6 +32,7 @@ def test_prover_modus_ponens(self): self.assertTrue(truth) def test_prover_modus_tollens(self): + """Tests the Modus Tollens rule of inference""" assumptions = ( ~self.q, IMPLY(self.p, self.q), @@ -40,6 +46,7 @@ def test_prover_modus_tollens(self): self.assertTrue(truth) def test_prover_hypothetical_syllogism(self): + """Tests the Hypothetical Syllogism rule of inference""" assumptions = ( IMPLY(self.p, self.q), IMPLY(self.q, self.r), @@ -53,6 +60,7 @@ def test_prover_hypothetical_syllogism(self): self.assertTrue(truth) def test_prover_disjunctive_syllogism(self): + """Tests the Disjunctive Syllogism rule of inference""" # (p ∨ q) ^ ¬ q -> p assumptions = ( self.p | self.q, @@ -80,6 +88,7 @@ def test_prover_disjunctive_syllogism(self): self.assertTrue(truth) def test_prover_addition(self): + """Tests the Addition rule of inference""" assumptions = (self.p,) conclusion = self.p | self.q @@ -98,6 +107,7 @@ def test_prover_addition(self): self.assertTrue(truth) def test_prover_simplification(self): + """Tests the Simplification rule of inference""" assumptions = (self.p & self.q,) conclusion = self.p @@ -116,6 +126,7 @@ def test_prover_simplification(self): self.assertTrue(truth) def test_prover_conjunction(self): + """Tests the Conjunction rule of inference""" assumptions = (self.p, self.q) conclusion = self.p & self.q @@ -134,6 +145,7 @@ def test_prover_conjunction(self): self.assertTrue(truth) def test_prover_resolution(self): + """Tests the Resolution rule of inference""" assumptions = ( self.p | self.q, ~self.p | self.r, @@ -147,6 +159,7 @@ def test_prover_resolution(self): self.assertTrue(truth) def test_prover_demorgans_theorem(self): + """Tests the De'Morgan's Theorem equivalence""" _, truth = Prover( (~self.x | ~self.y,), ~(self.x & self.y), @@ -172,10 +185,13 @@ def test_prover_demorgans_theorem(self): self.assertTrue(truth) def test_prover_not_of_not(self): + """Tests the Not of Not equivalence""" _, truth = Prover((~(~self.p),), self.p).prove() self.assertTrue(truth) def test_prover_complement(self): + """Tests the Complement equivalence + i.e. p | ~p is tautology and p & ~p is a contradiction""" _, truth = Prover(tuple(), self.p | ~self.p).prove() self.assertTrue(truth) @@ -183,6 +199,7 @@ def test_prover_complement(self): self.assertFalse(truth) def test_prover_definition_of_biconditional(self): + """Tests the Definition of Bi-Conditional equivalence""" assumption = (IFF(self.p, self.q),) conclusion = IMPLY(self.p, self.q) @@ -204,7 +221,9 @@ def test_prover_definition_of_biconditional(self): self.assertTrue(truth) def test_prover_multi_step_1(self): - # conjunction then demorgans + """Tests the multi step proof + with conjunction then demorgans""" + assumptions = (~self.x, ~self.y) conclusion = ~(self.x | self.y) @@ -215,7 +234,8 @@ def test_prover_multi_step_1(self): self.assertTrue(truth) def test_prover_multi_step_2(self): - # modus tollens then demorgans + """Tests the multi step proof + with modus tollens then demorgans""" assumptions = (IMPLY(self.x, self.y), ~self.y) conclusion = ~(self.x | self.y) @@ -226,7 +246,8 @@ def test_prover_multi_step_2(self): self.assertTrue(truth) def test_prover_multi_step_3(self): - # modus tollens then demorgans + """Tests the multi step proof + with modus tollens then demorgans""" assumptions = (IMPLY(self.x, self.y), ~self.y) conclusion = ~(self.x | self.y) @@ -246,10 +267,8 @@ def test_prover_multi_step_3(self): self.assertTrue(truth) def test_prove_superman_does_not_exists(self): - # based on the following question - # Taken from Discrete Mathematics and Its Applications 7th Edition - # by Kenneth H. Rosen - """ + """Tests the multi step proof + QUESTION: If Superman were able and willing to prevent evil, he would do so. If Superman were unable to prevent @@ -258,6 +277,9 @@ def test_prove_superman_does_not_exists(self): does not prevent evil. If Superman exists, he is neither impotent nor malevolent. Therefore, Superman does not exist. + + Taken from Discrete Mathematics and Its Applications 7th Edition + by Kenneth H. Rosen """ a = Proposition("a", "Superman is able to prevent evil")