Skip to content

Commit

Permalink
replaced Assumption.get with Assumption.add
Browse files Browse the repository at this point in the history
  • Loading branch information
@Vipul-Cariappa
Vipul-Cariappa committed Oct 24, 2023
1 parent 9e1df60 commit 1e0e111
Showing 1 changed file with 33 additions and 41 deletions.
74 changes: 33 additions & 41 deletions logic/proof.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ def __str__(self) -> str:


class Assumption:
def __init__(self, assumptions: Sequence[Statement] | AssumptionT) -> None:
def __init__(self, assumptions: Sequence[Statement] | set[Statement] | AssumptionT) -> None:
if isinstance(assumptions, Assumption):
self.assumptions: set[Statement] = set(assumptions.assumptions)
else:
Expand All @@ -74,11 +74,11 @@ def with_proposition(self, prop: Statement) -> Generator[Statement, None, None]:
if not yielded and prop in i:
yield i

def get(self) -> list[Statement]:
return list(self.assumptions)
def remove(self, *statement: Statement) -> AssumptionT:
return Assumption(self.assumptions - {*statement})

def remove(self, statement: Statement) -> AssumptionT:
return Assumption(list(self.assumptions - {statement}))
def add(self, *statement: Statement) -> AssumptionT:
return Assumption(self.assumptions.union({*statement}))


class Proof:
Expand Down Expand Up @@ -221,10 +221,10 @@ def prove(self) -> tuple[Proof, bool]:
# Applying NotOfNot i.e. ~(~x) <-> x
if isinstance(statement, CompositePropositionNOT):
if statement.statement != self.conclusion:
assumptions = self.assumptions.get()
if not (statement.statement in assumptions):
assumptions.append(statement.statement)
proof, truth = Prover(assumptions, self.conclusion).prove()
if not (statement.statement in self.assumptions):
proof, truth = Prover(
self.assumptions.add(statement.statement), self.conclusion
).prove()
if truth:
self.proof.add_step(self.conclusion, Equivalence.NotOfNot, i)
self.proof.extend(proof)
Expand All @@ -237,10 +237,10 @@ def prove(self) -> tuple[Proof, bool]:
match statement:
case CompositePropositionAND(first=first, second=second):
if (~first | ~second) != self.conclusion:
assumptions = self.assumptions.get()
if not ((~first | ~second) in assumptions):
assumptions.append(~first | ~second)
proof, truth = Prover(assumptions, self.conclusion).prove()
if not ((~first | ~second) in self.assumptions):
proof, truth = Prover(
self.assumptions.add(~first | ~second), self.conclusion
).prove()
if truth:
self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, i)
self.proof.extend(proof)
Expand All @@ -251,10 +251,10 @@ def prove(self) -> tuple[Proof, bool]:

case CompositePropositionOR(first=first, second=second):
if ~first & ~second != self.conclusion:
assumptions = self.assumptions.get()
if not ((~first & ~second) in assumptions):
assumptions.append(~first & ~second)
proof, truth = Prover(assumptions, self.conclusion).prove()
if not ((~first & ~second) in self.assumptions):
proof, truth = Prover(
self.assumptions.add(~first & ~second), self.conclusion
).prove()
if truth:
self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, i)
self.proof.extend(proof)
Expand Down Expand Up @@ -312,10 +312,10 @@ def prove(self) -> tuple[Proof, bool]:
# Applying De'Morgen's Law
if isinstance(first, CompositePropositionNOT) and isinstance(second, CompositePropositionNOT):
if ~(first.statement & second.statement) != self.conclusion:
assumptions = self.assumptions.get()
if not (~(first.statement & second.statement) in assumptions):
assumptions.append(~(first.statement & second.statement))
proof, truth = Prover(assumptions, self.conclusion).prove()
if not (~(first.statement & second.statement) in self.assumptions):
proof, truth = Prover(
self.assumptions.add(~(first.statement & second.statement)), self.conclusion
).prove()
if truth:
self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, i)
self.proof.extend(proof)
Expand All @@ -328,10 +328,10 @@ def prove(self) -> tuple[Proof, bool]:
# Applying De'Morgen's Law
if isinstance(first, CompositePropositionNOT) and isinstance(second, CompositePropositionNOT):
if ~(first.statement | second.statement) != self.conclusion:
assumptions = self.assumptions.get()
if not (~(first.statement | second.statement) in assumptions):
assumptions.append(~(first.statement | second.statement))
proof, truth = Prover(assumptions, self.conclusion).prove()
if not (~(first.statement | second.statement) in self.assumptions):
proof, truth = Prover(
self.assumptions.add(~(first.statement | second.statement)), self.conclusion
).prove()
if truth:
self.proof.add_step(self.conclusion, Equivalence.DeMorgensLaw, i)
self.proof.extend(proof)
Expand All @@ -341,14 +341,9 @@ def prove(self) -> tuple[Proof, bool]:
return self.proof, True

# Applying Simplification
assumptions = self.assumptions.get()

if first != self.conclusion and second != self.conclusion:
if not (first in assumptions) or not (second in assumptions):
assumptions.append(first)
assumptions.append(second)

proof, truth = Prover(assumptions, self.conclusion).prove()
if not (first in self.assumptions) or not (second 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.extend(proof)
Expand All @@ -370,7 +365,7 @@ def prove(self) -> tuple[Proof, bool]:
self.proof.add_step(conclusion, RulesOfInference.ModusPonens, i, assumption)
if self.conclusion != conclusion:
proof, truth = Prover(
[conclusion, *(self.assumptions.remove(i).get())], self.conclusion
self.assumptions.remove(i).add(conclusion), self.conclusion
).prove()
if truth:
self.proof.extend(proof)
Expand All @@ -390,7 +385,7 @@ def prove(self) -> tuple[Proof, bool]:
self.proof.add_step(~assumption, RulesOfInference.ModusTollens, i, ~conclusion)
if self.conclusion != ~assumption:
proof, truth = Prover(
[~assumption, *(self.assumptions.remove(i).get())], self.conclusion
self.assumptions.remove(i).add(~assumption), self.conclusion
).prove()
if truth:
self.proof.extend(proof)
Expand Down Expand Up @@ -425,15 +420,12 @@ def prove(self) -> tuple[Proof, bool]:
self.proof.add_step(self.conclusion, Equivalence.DefinitionOfBiConditional, i)
return self.proof, True

assumptions = self.assumptions.get()
if (not (IMPLY(assumption, conclusion) in assumptions)) or (
not (IMPLY(conclusion, assumption) in assumptions)
if (not (IMPLY(assumption, conclusion) in self.assumptions)) or (
not (IMPLY(conclusion, assumption) in self.assumptions)
):
proof, truth = Prover(
(
IMPLY(conclusion, assumption),
IMPLY(assumption, conclusion),
*self.assumptions.remove(i).assumptions,
self.assumptions.remove(i).add(
IMPLY(conclusion, assumption), IMPLY(assumption, conclusion)
),
self.conclusion,
).prove()
Expand Down

0 comments on commit 1e0e111

Please sign in to comment.