diff --git a/logic/proof.py b/logic/proof.py index d148e5d..69ca295 100644 --- a/logic/proof.py +++ b/logic/proof.py @@ -15,7 +15,18 @@ ProofT: TypeAlias = "Proof" -class RulesOfInference(Enum): +class ProofStrategy(Enum): + pass + + +class Equivalence(ProofStrategy): + DefinitionOfBiConditional = "Definition Of Bi-Conditional" + DeMorgensLaw = "De'Morgen's Law" + NotOfNot = "NotOfNot" + Complement = "Complement" + + +class RulesOfInference(ProofStrategy): ModusPonens = "Modus Ponens" ModusTollens = "Modus Tollens" HypotheticalSyllogism = "Hypothetical Syllogism" @@ -25,8 +36,6 @@ class RulesOfInference(Enum): Conjunction = "Conjunction" Resolution = "Resolution" Deduction = "Deduction" - DefinitionOfBiConditional = "Definition Of Bi-Conditional" - DeMorgensLaw = "De'Morgen's Law" class Assumption: @@ -59,16 +68,16 @@ def remove(self, statement: Statement) -> AssumptionT: class Proof: - def __init__(self) -> None: - self.proof: list[tuple[RulesOfInference, tuple[Statement, ...]]] = [] + def __init__(self, proof: list[tuple[ProofStrategy, tuple[Statement, ...]]] | None = None) -> None: + self.proof: list[tuple[ProofStrategy, tuple[Statement, ...]]] = proof if proof else [] - def add(self, roi: RulesOfInference, *statement: Statement) -> None: + def add(self, roi: ProofStrategy, *statement: Statement) -> None: self.proof.append((roi, (*statement,))) def extend(self, proof: ProofT) -> None: self.proof.extend(proof.proof) - def __iter__(self) -> Iterator[tuple[RulesOfInference, tuple[Statement, ...]]]: + def __iter__(self) -> Iterator[tuple[ProofStrategy, tuple[Statement, ...]]]: return iter(self.proof) def __str__(self) -> str: @@ -86,11 +95,6 @@ def __init__( assumptions: Sequence[Statement] | Assumption, conclusion: Statement, ) -> None: - # if not isinstance(conclusion, Proposition): - # raise NotImplementedError( - # "Proving where the conclusion is Composite Proposition is not yet implemented." - # ) - if isinstance(assumptions, Assumption): self.assumptions = assumptions else: @@ -100,25 +104,35 @@ def __init__( def _prove_decomposed_conclusion(self) -> tuple[Proof, bool]: match self.conclusion: - case CompositePropositionAND(first=first, second=second): - # 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() - if truth_first and truth_second: - self.proof.extend(proof_first) - self.proof.extend(proof_second) - self.proof.add(RulesOfInference.Conjunction, first, second) - return self.proof, True - - # Applying De'Morgen's Law - if isinstance(first, CompositePropositionNOT) and isinstance(second, CompositePropositionNOT): - proof, truth = Prover(self.assumptions, ~(first | second)).prove() + case CompositePropositionNOT(statement=statement): + # Applying NotOfNot i.e. ~(~x) <-> x + if isinstance(statement, CompositePropositionNOT): + proof, truth = Prover(self.assumptions, statement.statement).prove() if truth: self.proof.extend(proof) - self.proof.add(RulesOfInference.DeMorgensLaw, ~(first | second)) + self.proof.add(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() + if truth: + self.proof.extend(proof) + self.proof.add(Equivalence.DeMorgensLaw, ~first | ~second) + return self.proof, True + case CompositePropositionOR(first=first, second=second): + proof, truth = Prover(self.assumptions, ~first & ~second).prove() + if truth: + self.proof.extend(proof) + self.proof.add(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([(Equivalence.Complement, (self.conclusion,))]), True + # Applying Addition proof_first, truth_first = Prover(self.assumptions.remove(self.conclusion), first).prove() if truth_first: @@ -136,7 +150,29 @@ def _prove_decomposed_conclusion(self) -> tuple[Proof, bool]: proof, truth = Prover(self.assumptions, ~(first & second)).prove() if truth: self.proof.extend(proof) - self.proof.add(RulesOfInference.DeMorgensLaw, ~(first & second)) + self.proof.add(Equivalence.DeMorgensLaw, ~(first & second)) + return self.proof, True + + case CompositePropositionAND(first=first, second=second): + # Applying x & ~x <-> False + if first == ~second or ~first == second: + 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() + if truth_first and truth_second: + self.proof.extend(proof_first) + self.proof.extend(proof_second) + self.proof.add(RulesOfInference.Conjunction, first, second) + return self.proof, True + + # Applying De'Morgen's Law + 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(Equivalence.DeMorgensLaw, ~(first | second)) return self.proof, True case CompositePropositionBICONDITIONAL(assumption=assumption, conclusion=conclusion): @@ -152,28 +188,12 @@ def _prove_decomposed_conclusion(self) -> tuple[Proof, bool]: self.proof.extend(proof_p_implies_q) self.proof.extend(proof_q_implies_p) self.proof.add( - RulesOfInference.DefinitionOfBiConditional, + Equivalence.DefinitionOfBiConditional, IMPLY(assumption, conclusion), IMPLY(conclusion, assumption), ) return self.proof, True - case CompositePropositionNOT(statement=statement): - # Applying De'Morgen's Law - match statement: - case CompositePropositionAND(first=first, second=second): - proof, truth = Prover(self.assumptions, ~first | ~second).prove() - if truth: - self.proof.extend(proof) - self.proof.add(RulesOfInference.DeMorgensLaw, ~first | ~second) - return self.proof, True - case CompositePropositionOR(first=first, second=second): - proof, truth = Prover(self.assumptions, ~first & ~second).prove() - if truth: - self.proof.extend(proof) - self.proof.add(RulesOfInference.DeMorgensLaw, ~first & ~second) - return self.proof, True - return Proof(), False def prove(self) -> tuple[Proof, bool]: @@ -183,75 +203,61 @@ def prove(self) -> tuple[Proof, bool]: return self.proof, True match i: - case CompositePropositionCONDITIONAL(assumption=assumption, conclusion=conclusion): - # Applying Modus Ponens - if ( - (not (conclusion in self.assumptions)) - and self.conclusion != assumption - and self.conclusion != ~conclusion - ): - proof, truth = Prover(self.assumptions.remove(i), assumption).prove() - if truth: - self.proof.extend(proof) - self.proof.add(RulesOfInference.ModusPonens, i, assumption) - proof, truth = Prover( - [conclusion, *(self.assumptions.remove(i).get())], self.conclusion - ).prove() - if truth: - self.proof.extend(proof) - return self.proof, True - - # Applying Modus Tollens - if ( - (not (~assumption in self.assumptions)) - and self.conclusion != ~conclusion - and self.conclusion != assumption - ): - proof, truth = Prover(self.assumptions.remove(i), ~conclusion).prove() - if truth: - self.proof.extend(proof) - self.proof.add(RulesOfInference.ModusTollens, i, ~conclusion) - proof, truth = Prover( - [~assumption, *(self.assumptions.remove(i).get())], self.conclusion - ).prove() + case CompositePropositionNOT(statement=statement): + # Applying NotOfNot i.e. ~(~x) <-> x + if isinstance(statement, CompositePropositionNOT): + assumptions = self.assumptions.get() + if not (statement.statement in assumptions): + assumptions.append(statement.statement) + proof, truth = Prover(assumptions, self.conclusion).prove() if truth: + self.proof.add(Equivalence.NotOfNot, i) self.proof.extend(proof) return self.proof, True - # Applying Hypothetical Syllogism - if isinstance(self.conclusion, CompositePropositionCONDITIONAL): - if self.conclusion.conclusion == conclusion: - proof, truth = Prover( - self.assumptions.remove(i), - IMPLY(self.conclusion.assumption, assumption), - ).prove() - if truth: - self.proof.extend(proof) - self.proof.add(RulesOfInference.HypotheticalSyllogism, i) - return self.proof, True + # Applying De'Morgan's Law + match statement: + case CompositePropositionAND(first=first, second=second): + assumptions = self.assumptions.get() + if not ((~first | ~second) in assumptions): + assumptions.append(~first | ~second) + proof, truth = Prover(assumptions, self.conclusion).prove() + if truth: + self.proof.add(Equivalence.DeMorgensLaw, i) + self.proof.extend(proof) + return proof, True + case CompositePropositionOR(first=first, second=second): + assumptions = self.assumptions.get() + if not ((~first & ~second) in assumptions): + assumptions.append(~first & ~second) + proof, truth = Prover(assumptions, self.conclusion).prove() + if truth: + self.proof.add(Equivalence.DeMorgensLaw, i) + self.proof.extend(proof) + 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() - self.proof.add(RulesOfInference.Resolution, i) self.proof.extend(proof) + self.proof.add(RulesOfInference.Resolution, i) return self.proof, True if self.conclusion.second == second: proof, truth = Prover(self.assumptions.remove(i), ~first | self.conclusion.first).prove() - self.proof.add(RulesOfInference.Resolution, i) self.proof.extend(proof) + self.proof.add(RulesOfInference.Resolution, i) return self.proof, True if self.conclusion.first == second: proof, truth = Prover(self.assumptions.remove(i), ~first | self.conclusion.second).prove() - self.proof.add(RulesOfInference.Resolution, i) self.proof.extend(proof) + self.proof.add(RulesOfInference.Resolution, i) return self.proof, True if self.conclusion.second == first: proof, truth = Prover(self.assumptions.remove(i), ~second | self.conclusion.first).prove() - self.proof.add(RulesOfInference.Resolution, i) self.proof.extend(proof) + self.proof.add(RulesOfInference.Resolution, i) return self.proof, True # Applying Disjunctive Syllogism @@ -275,7 +281,7 @@ def prove(self) -> tuple[Proof, bool]: assumptions.append(~(first.statement & second.statement)) proof, truth = Prover(assumptions, self.conclusion).prove() if truth: - self.proof.add(RulesOfInference.DeMorgensLaw, i) + self.proof.add(Equivalence.DeMorgensLaw, i) self.proof.extend(proof) return self.proof, True @@ -300,10 +306,57 @@ def prove(self) -> tuple[Proof, bool]: assumptions.append(~(first.statement | second.statement)) proof, truth = Prover(assumptions, self.conclusion).prove() if truth: - self.proof.add(RulesOfInference.DeMorgensLaw, i) + self.proof.add(Equivalence.DeMorgensLaw, i) self.proof.extend(proof) return self.proof, True + case CompositePropositionCONDITIONAL(assumption=assumption, conclusion=conclusion): + # Applying Modus Ponens + if ( + (not (conclusion in self.assumptions)) + and self.conclusion != assumption + and self.conclusion != ~conclusion + ): + proof, truth = Prover(self.assumptions.remove(i), assumption).prove() + if truth: + self.proof.extend(proof) + self.proof.add(RulesOfInference.ModusPonens, i, assumption) + proof, truth = Prover( + [conclusion, *(self.assumptions.remove(i).get())], self.conclusion + ).prove() + if truth: + self.proof.extend(proof) + return self.proof, True + + # Applying Modus Tollens + if ( + (not (~assumption in self.assumptions)) + and self.conclusion != ~conclusion + and self.conclusion != assumption + ): + proof, truth = Prover(self.assumptions.remove(i), ~conclusion).prove() + if truth: + self.proof.extend(proof) + self.proof.add(RulesOfInference.ModusTollens, i, ~conclusion) + proof, truth = Prover( + [~assumption, *(self.assumptions.remove(i).get())], self.conclusion + ).prove() + if truth: + self.proof.extend(proof) + return self.proof, True + + # Applying Hypothetical Syllogism + if isinstance(self.conclusion, CompositePropositionCONDITIONAL): + if self.conclusion.conclusion == conclusion: + proof, truth = Prover( + self.assumptions.remove(i), + IMPLY(self.conclusion.assumption, assumption), + ).prove() + if truth: + self.proof.extend(proof) + self.proof.add(RulesOfInference.HypotheticalSyllogism, i) + return self.proof, True + case CompositePropositionBICONDITIONAL(assumption=assumption, conclusion=conclusion): # Applying definition of Bi-Conditional # (p <-> q) -> (p -> q) & (q -> p) @@ -316,30 +369,8 @@ def prove(self) -> tuple[Proof, bool]: proof, truth = Prover(assumptions, self.conclusion).prove() if truth: - self.proof.add(RulesOfInference.DefinitionOfBiConditional, i) + self.proof.add(Equivalence.DefinitionOfBiConditional, i) self.proof.extend(proof) return self.proof, True - case CompositePropositionNOT(statement=statement): - # Applying De'Morgan's Law - match statement: - case CompositePropositionAND(first=first, second=second): - assumptions = self.assumptions.get() - if not ((~first | ~second) in assumptions): - assumptions.append(~first | ~second) - proof, truth = Prover(assumptions, self.conclusion).prove() - if truth: - self.proof.add(RulesOfInference.DeMorgensLaw, i) - self.proof.extend(proof) - return proof, True - case CompositePropositionOR(first=first, second=second): - assumptions = self.assumptions.get() - if not ((~first & ~second) in assumptions): - assumptions.append(~first & ~second) - proof, truth = Prover(assumptions, self.conclusion).prove() - if truth: - self.proof.add(RulesOfInference.DeMorgensLaw, i) - self.proof.extend(proof) - return self.proof, True - return self._prove_decomposed_conclusion()