Skip to content

Commit

Permalink
implemented more tests for:
Browse files Browse the repository at this point in the history 
also fixed failing tests and generating of proof is prettier

- Not Of Not
- Complement
- Definition of Bi-Conditional
  • Loading branch information
@Vipul-Cariappa
Vipul-Cariappa committed Oct 23, 2023
1 parent 985de5f commit f746251
Show file tree
Hide file tree
Showing 2 changed files with 155 additions and 71 deletions.
192 changes: 122 additions & 70 deletions logic/proof.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -206,109 +206,140 @@ def prove(self) -> tuple[Proof, bool]:
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 De'Morgan's Law
match statement:
case CompositePropositionAND(first=first, second=second):
if statement.statement != self.conclusion:
assumptions = self.assumptions.get()
if not ((~first | ~second) in assumptions):
assumptions.append(~first | ~second)
if not (statement.statement in assumptions):
assumptions.append(statement.statement)
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.add(Equivalence.NotOfNot, i)
self.proof.extend(proof)
return self.proof, True
else:
self.proof.add(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:
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
else:
self.proof.add(Equivalence.DeMorgensLaw, i)
return self.proof, True

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 truth:
self.proof.add(Equivalence.DeMorgensLaw, i)
self.proof.extend(proof)
return self.proof, True
else:
self.proof.add(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()
self.proof.extend(proof)
self.proof.add(RulesOfInference.Resolution, i)
self.proof.add(RulesOfInference.Deduction, i)
self.proof.add(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()
self.proof.extend(proof)
self.proof.add(RulesOfInference.Resolution, i)
self.proof.add(RulesOfInference.Deduction, i)
self.proof.add(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()
self.proof.extend(proof)
self.proof.add(RulesOfInference.Resolution, i)
self.proof.add(RulesOfInference.Deduction, i)
self.proof.add(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()
self.proof.extend(proof)
self.proof.add(RulesOfInference.Resolution, i)
self.proof.add(RulesOfInference.Deduction, i)
self.proof.add(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()
if truth:
self.proof.extend(proof)
self.proof.add(RulesOfInference.DisjunctiveSyllogism, i)
self.proof.add(RulesOfInference.Deduction, i)
self.proof.add(RulesOfInference.DisjunctiveSyllogism, i, ~second)
return self.proof, True
if self.conclusion == second:
proof, truth = Prover(self.assumptions.remove(i), ~first).prove()
if truth:
self.proof.extend(proof)
self.proof.add(RulesOfInference.DisjunctiveSyllogism, i)
self.proof.add(RulesOfInference.Deduction, i)
self.proof.add(RulesOfInference.DisjunctiveSyllogism, i, ~first)
return self.proof, True

# Applying De'Morgen's Law
if isinstance(first, CompositePropositionNOT) and isinstance(second, CompositePropositionNOT):
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 truth:
self.proof.add(Equivalence.DeMorgensLaw, i)
self.proof.extend(proof)
return self.proof, True
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 truth:
self.proof.add(Equivalence.DeMorgensLaw, i)
self.proof.extend(proof)
return self.proof, True
else:
self.proof.add(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 ~(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 truth:
self.proof.add(Equivalence.DeMorgensLaw, i)
self.proof.extend(proof)
return self.proof, True
else:
self.proof.add(Equivalence.DeMorgensLaw, i)
return self.proof, True

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

if not (first in assumptions) or not (second in assumptions):
assumptions.append(first)
assumptions.append(second)
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 truth:
self.proof.add(RulesOfInference.Simplification, i)
self.proof.extend(proof)
return self.proof, True

# Applying De'Morgen's Law
if isinstance(first, CompositePropositionNOT) and isinstance(second, CompositePropositionNOT):
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 truth:
self.proof.add(Equivalence.DeMorgensLaw, i)
self.proof.add(RulesOfInference.Simplification, i)
self.proof.extend(proof)
return self.proof, True
else:
self.proof.add(RulesOfInference.Simplification, i)
return self.proof, True

case CompositePropositionCONDITIONAL(assumption=assumption, conclusion=conclusion):
# Applying Modus Ponens
Expand All @@ -320,12 +351,16 @@ def prove(self) -> tuple[Proof, bool]:
proof, truth = Prover(self.assumptions.remove(i), assumption).prove()
if truth:
self.proof.extend(proof)
self.proof.add(RulesOfInference.Deduction, i)
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)
if self.conclusion != conclusion:
proof, truth = Prover(
[conclusion, *(self.assumptions.remove(i).get())], self.conclusion
).prove()
if truth:
self.proof.extend(proof)
return self.proof, True
else:
return self.proof, True

# Applying Modus Tollens
Expand All @@ -337,12 +372,16 @@ def prove(self) -> tuple[Proof, bool]:
proof, truth = Prover(self.assumptions.remove(i), ~conclusion).prove()
if truth:
self.proof.extend(proof)
self.proof.add(RulesOfInference.Deduction, i)
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)
if self.conclusion != ~assumption:
proof, truth = Prover(
[~assumption, *(self.assumptions.remove(i).get())], self.conclusion
).prove()
if truth:
self.proof.extend(proof)
return self.proof, True
else:
return self.proof, True

# Applying Hypothetical Syllogism
Expand All @@ -354,20 +393,33 @@ def prove(self) -> tuple[Proof, bool]:
).prove()
if truth:
self.proof.extend(proof)
self.proof.add(RulesOfInference.HypotheticalSyllogism, i)
self.proof.add(RulesOfInference.Deduction, i)
self.proof.add(
RulesOfInference.HypotheticalSyllogism,
i,
IMPLY(self.conclusion.assumption, assumption),
)
return self.proof, True

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(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 assumptions)) or (
not (IMPLY(conclusion, assumption) in assumptions)
):
assumptions.append(IMPLY(assumption, conclusion))
assumptions.append(IMPLY(conclusion, assumption))

proof, truth = Prover(assumptions, self.conclusion).prove()
proof, truth = Prover(
(
IMPLY(conclusion, assumption),
IMPLY(assumption, conclusion),
*self.assumptions.remove(i).assumptions,
),
self.conclusion,
).prove()
if truth:
self.proof.add(Equivalence.DefinitionOfBiConditional, i)
self.proof.extend(proof)
Expand Down
34 changes: 33 additions & 1 deletion tests/test_prover.py
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import unittest
from logic import Proposition, Prover, IMPLY
from logic import Proposition, Prover, IMPLY, IFF

# TODO: check proof

Expand Down Expand Up @@ -171,6 +171,38 @@ def test_prover_demorgans_theorem(self):
).prove()
self.assertTrue(truth)

def test_prover_not_of_not(self):
_, truth = Prover((~(~self.p),), self.p).prove()
self.assertTrue(truth)

def test_prover_complement(self):
_, truth = Prover(tuple(), self.p | ~self.p).prove()
self.assertTrue(truth)

_, truth = Prover(tuple(), self.p & ~self.p).prove()
self.assertFalse(truth)

def test_prover_definition_of_biconditional(self):
assumption = (IFF(self.p, self.q),)

conclusion = IMPLY(self.p, self.q)
_, truth = Prover(assumption, conclusion).prove()
self.assertTrue(truth)

conclusion = IMPLY(self.q, self.p)
_, truth = Prover(assumption, conclusion).prove()
self.assertTrue(truth)

assumption = (IMPLY(self.p, self.q), IMPLY(self.q, self.p))

conclusion = IFF(self.p, self.q)
_, truth = Prover(assumption, conclusion).prove()
self.assertTrue(truth)

conclusion = IFF(self.q, self.p)
_, truth = Prover(assumption, conclusion).prove()
self.assertTrue(truth)

def test_prover_multi_step_1(self):
# conjunction then demorgans
assumptions = (~self.x, ~self.y)
Expand Down

0 comments on commit f746251

Please sign in to comment.