added composition helper functions: AND, OR, NOT, IFF, IMPLY

.gitignore

@@ -177,3 +177,6 @@ pyrightconfig.json
 
 # vscode
 .vscode/
+
+# temparary folder
+tmp/

logic/__init__.py

@@ -1,8 +1,4 @@
 from .proof import Prover, Proof
-from .proposition import Proposition
+from .proposition import Proposition, IMPLY, IFF, AND, OR, NOT
 
-__all__ = [
-    "Proposition",
-    "Proof",
-    "Prover"
-]
+__all__ = ["Proposition", "Proof", "Prover", "IMPLY", "IFF", "AND", "OR", "NOT"]

logic/proof.py

@@ -6,6 +6,7 @@
     CompositePropositionOR,
     CompositePropositionBICONDITIONAL,
     CompositePropositionCONDITIONAL,
+    IMPLY,
 )
 
 from enum import Enum
@@ -142,18 +143,18 @@ def _prove_decomposed_conclusion(self) -> tuple[Proof, bool]:
                 # 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), 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), 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)
                     self.proof.extend(proof_q_implies_p)
                     self.proof.add(
                         RulesOfInference.DefinitionOfBiConditional,
-                        assumption / conclusion,
-                        conclusion / assumption,
+                        IMPLY(assumption, conclusion),
+                        IMPLY(conclusion, assumption),
                     )
                     return self.proof, True
 
@@ -222,7 +223,7 @@ def prove(self) -> tuple[Proof, bool]:
                         if self.conclusion.conclusion == conclusion:
                             proof, truth = Prover(
                                 self.assumptions.remove(i),
-                                self.conclusion.assumption / assumption,
+                                IMPLY(self.conclusion.assumption, assumption),
                             ).prove()
                             if truth:
                                 self.proof.extend(proof)
@@ -307,9 +308,11 @@ def prove(self) -> tuple[Proof, bool]:
                     # Applying definition of Bi-Conditional
                     #  (p <-> q) -> (p -> q) & (q -> p)
                     assumptions = self.assumptions.get()
-                    if not ((assumption / conclusion) in assumptions) or not ((conclusion / assumption) in assumptions):
-                        assumptions.append(assumption / conclusion)
-                        assumptions.append(conclusion / assumption)
+                    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()
                         if truth:

logic/proposition.py

@@ -42,16 +42,6 @@ def __invert__(self) -> StatementT:
             return copy(self.statement)
         return CompositePropositionNOT(self)
 
-    def __truediv__(self, other: Any) -> StatementT:
-        if not isinstance(other, Statement):
-            raise TypeError(f"Cannot perform logical imply of {type(self)} with {type(other)}")
-        return CompositePropositionCONDITIONAL(self, other)
-
-    def __mod__(self, other: Any) -> StatementT:
-        if not isinstance(other, Statement):
-            raise TypeError(f"Cannot perform logical bi-conditional of {type(self)} with {type(other)}")
-        return CompositePropositionBICONDITIONAL(self, other)
-
 
 @dataclass(frozen=True)
 class Proposition(Statement):
@@ -233,8 +223,8 @@ class CompositePropositionBICONDITIONAL(CompositeProposition):
     conclusion: Statement
 
     def remove_conditionals(self) -> StatementT:
-        return (self.assumption / self.conclusion).remove_conditionals() & (
-            self.conclusion / self.assumption
+        return (IMPLY(self.assumption, self.conclusion)).remove_conditionals() & (
+            IMPLY(self.conclusion, self.assumption)
         ).remove_conditionals()
 
     def extract(self) -> list[PropositionT]:
@@ -263,3 +253,29 @@ def __eq__(self, other: Any) -> bool:
             return self.assumption == other.assumption and self.conclusion == other.conclusion
 
         return False
+
+
+def AND(first: Statement, second: Statement, *others: Statement) -> CompositePropositionAND:
+    if len(others) == 0:
+        return CompositePropositionAND(first, second)
+
+    return CompositePropositionAND(first, AND(second, *others))
+
+
+def OR(first: Statement, second: Statement, *others: Statement) -> CompositePropositionOR:
+    if len(others) == 0:
+        return CompositePropositionOR(first, second)
+
+    return CompositePropositionOR(first, OR(second, *others))
+
+
+def NOT(statement: Statement) -> CompositePropositionNOT:
+    return CompositePropositionNOT(statement)
+
+
+def IMPLY(assumption: Statement, conclusion: Statement) -> CompositePropositionCONDITIONAL:
+    return CompositePropositionCONDITIONAL(assumption, conclusion)
+
+
+def IFF(assumption: Statement, conclusion: Statement) -> CompositePropositionBICONDITIONAL:
+    return CompositePropositionBICONDITIONAL(assumption, conclusion)

tests/test_prover.py

@@ -1,5 +1,5 @@
 import unittest
-from logic import Proposition, Prover
+from logic import Proposition, Prover, IMPLY
 
 # TODO: check proof
 
@@ -16,7 +16,7 @@ def setUp(self) -> None:
     def test_prover_modus_ponens(self):
         assumptions = (
             self.p,
-            self.p / self.q,
+            IMPLY(self.p, self.q),
         )
         conclusion = self.q
 
@@ -29,7 +29,7 @@ def test_prover_modus_ponens(self):
     def test_prover_modus_tollens(self):
         assumptions = (
             ~self.q,
-            self.p / self.q,
+            IMPLY(self.p, self.q),
         )
         conclusion = ~self.p
 
@@ -41,10 +41,10 @@ def test_prover_modus_tollens(self):
 
     def test_prover_hypothetical_syllogism(self):
         assumptions = (
-            self.p / self.q,
-            self.q / self.r,
+            IMPLY(self.p, self.q),
+            IMPLY(self.q, self.r),
         )
-        conclusion = self.p / self.r
+        conclusion = IMPLY(self.p, self.r)
 
         _, truth = Prover(
             assumptions,
@@ -184,7 +184,7 @@ def test_prover_multi_step_1(self):
 
     def test_prover_multi_step_2(self):
         # modus tollens then demorgans
-        assumptions = (self.x / self.y, ~self.y)
+        assumptions = (IMPLY(self.x, self.y), ~self.y)
         conclusion = ~(self.x | self.y)
 
         _, truth = Prover(
@@ -195,7 +195,7 @@ def test_prover_multi_step_2(self):
 
     def test_prover_multi_step_3(self):
         # modus tollens then demorgans
-        assumptions = (self.x / self.y, ~self.y)
+        assumptions = (IMPLY(self.x, self.y), ~self.y)
         conclusion = ~(self.x | self.y)
 
         _, truth = Prover(
@@ -204,7 +204,7 @@ def test_prover_multi_step_3(self):
         ).prove()
         self.assertTrue(truth)
 
-        assumptions = ((self.y | self.z) / self.x, ~self.x)
+        assumptions = (IMPLY(self.y | self.z, self.x), ~self.x)
         conclusion = ~self.y & ~self.z
 
         _, truth = Prover(
@@ -236,11 +236,11 @@ def test_prove_superman_does_not_exists(self):
         f = Proposition("g", "Superman exists")
 
         assumptions = [
-            (a & b) / e,
-            (~e) / c,
-            (~b) / d,
+            IMPLY(a & b, e),
+            IMPLY(~e, c),
+            IMPLY(~b, d),
             ~e,
-            f / (~c & ~d),
+            IMPLY(f, ~c & ~d),
         ]
         conclusion = ~f