From 8f28384b4c00099ff4d046c7eb4a84e17e8c6937 Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Sat, 7 Sep 2013 18:49:14 +0200
Subject: [PATCH 01/19] Better implementation of the resolution method

- Insert preliminary steps.
- First interface of ClausePicker class

To be tested
---
 pylogic/propositional/resolution.py | 136 +++++++++++++++++++++-------
 1 file changed, 104 insertions(+), 32 deletions(-)

diff --git a/pylogic/propositional/resolution.py b/pylogic/propositional/resolution.py
index b35694f..702b1ad 100644
--- a/pylogic/propositional/resolution.py
+++ b/pylogic/propositional/resolution.py
@@ -3,6 +3,63 @@
 from pylogic import logic
 
 
+def preliminary_steps(clauses):
+    manage_tops(clauses)
+    manage_complementary(clauses)
+    manage_bottoms(clauses)
+    manage_copies(clauses)
+
+def manage_tops(clauses):
+    """Remove the clauses containg the top."""
+    removable = []
+    for c in range(len(clauses)):
+        clause = clauses[c]
+        for formula in clause.list:
+            if formula == Formula("T"):
+                removable.append(c)
+                break
+    for i in removable:
+        clauses.pop(i)
+
+def manage_complementary(clauses):
+    """Remove the clauses containing two complementary formulas."""
+    removable = []
+    for c in range(len(clauses)):
+        clause = clauses[c]
+        found == False
+        f = 0
+        while not found and f < len(clause.list):
+            formula1 = clause.list[f]
+            for f2 in range(f+1, len(clause.list)):
+                formula2 = clause.list[f2]
+                if formula1 == formula2.complement():
+                    removable.append(c)
+                    found = True
+                    break
+            f = f + 1
+    for i in removable:
+        clauses.pop(i)
+
+def manage_bottoms(clauses):
+    """Remove the bottoms from every clause."""
+    for clause in clauses:
+        clause.remove_every(Formula("F"))
+
+def manage_copies(clauses):
+    """Remove from every clause repetion of inner formulas."""
+    for clause in clauses:
+        f = 0
+        while f < len(clause.list):
+            formula = clause.list[f]
+            f2 = f+1
+            while f2 < len(clause.list):
+                formula2 = clause.list[f2]
+                if formula == formula2:
+                    clause.list.pop(f2)
+                else:
+                    f2 = f2+1
+
+
 def is_closed(expansion):
     """Given a list of clauses, return True if it contains an empty clause,
     False otherwise"""
@@ -14,33 +71,28 @@ def is_closed(expansion):
     return False
 
 
-def expand(expansion):
-    """Apply the resolution rule to the given expansion.
-    Returns True if the resolution rule is applied, False otherwise."""
-    # for each formula
-    for g in range(len(expansion)):
-        if expansion[g][0]:
-            continue
-        gen = expansion[g][1]
-        for f in range(len(gen.list)):
-            formula = gen.list[f]
-            # check if exists a complement of formula
-            # in the rest of the expansion
-            for ng in range(g+1, len(expansion)):
-                temp_gen = expansion[ng][1]
-                for nf in range(len(temp_gen.list)):
-                    temp_formula = temp_gen.list[nf]
-                    if formula == temp_formula.complement():
-                        gen = copy.deepcopy(gen)
-                        gen2 = copy.deepcopy(temp_gen)
-                        gen.remove_every(formula)
-                        gen2.remove_every(temp_formula)
-                        gen.list.extend(gen2.list)
-                        expansion.append([False, gen])
-                        expansion[g][0] = True
-                        return True
-                    # else ignore it
-    return False
+def resolution_rule(clause1, clause2, formula):
+    """Apply the resolution rule to the given clauses and formula."""
+    new_clause = copy.deepcopy(clause1)
+    other = copy.deepcopy(clause2)
+    new_clause.remove_every(formula)
+    other.remove_every(temp_formula)
+    new_clause.list.extend(other.list)
+    return new_clause
+
+
+def resolution_rule_exhaust(clause1, clause2):
+    """Apply the resolution rule to the given clauses
+    for every possible inner formulas"""
+    new_clauses = []
+    for f in range(len(clause1.list)):
+        formula = clause1.list[f]
+        # check if exists a complement of formula
+        for nf in range(len(clause2.list)):
+            temp_formula = clause2.list[nf]
+            if formula == temp_formula.complement():
+                clause = resolution_rule(clause1, clause2, formula)
+                new_clauses.append(clause)
 
 
 def is_tautology(formula):
@@ -52,13 +104,33 @@ def is_tautology(formula):
     negation = formula.negate()
     cnf = negation.cnf()
     print(cnf)
-    expansion = [[False, disj] for disj in cnf.list]
-    enough = False
-    while not is_closed(expansion) and not enough:
-        applied = expand(expansion)
-        enough = not applied
+    expansion = cnf.list
+    preliminary_steps(expansion)
+    picker = ClausePicker(expansion)
+    closed = is_closed(expansion)
+    while not closed and not picker.is_empty():
+        clauses = picker.pick()
+        new_clauses = resolution_rule_exhaust(clauses[0], clauses[1])
+        picker.update(expansion, new_clauses)
+        expansion.extend(new_clauses)
         disjs = ""
         for g in expansion:
             disjs = disjs + " " + g[1].__str__()
         print(disjs)
+        closed = is_closed(expansion)
     return is_closed(expansion)
+
+
+
+class ClausePicker():
+    def __init__(self, expansion):
+        pass
+
+    def pick(self):
+        return None
+
+    def add_clause(self, expansion, clause):
+        pass
+
+    def is_empty(self):
+        pass

From c225aeb244e0ef8741a0135dee2dc26b18891a21 Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Sun, 8 Sep 2013 11:00:39 +0200
Subject: [PATCH 02/19] Test preliminary steps

---
 pylogic/propositional/resolution.py           | 11 +--
 .../tests/test_propositional_resolution.py    | 82 ++++++++++++++++---
 2 files changed, 77 insertions(+), 16 deletions(-)

diff --git a/pylogic/propositional/resolution.py b/pylogic/propositional/resolution.py
index 702b1ad..c8aa4dd 100644
--- a/pylogic/propositional/resolution.py
+++ b/pylogic/propositional/resolution.py
@@ -18,7 +18,7 @@ def manage_tops(clauses):
             if formula == Formula("T"):
                 removable.append(c)
                 break
-    for i in removable:
+    for i in reversed(removable):
         clauses.pop(i)
 
 def manage_complementary(clauses):
@@ -26,7 +26,7 @@ def manage_complementary(clauses):
     removable = []
     for c in range(len(clauses)):
         clause = clauses[c]
-        found == False
+        found = False
         f = 0
         while not found and f < len(clause.list):
             formula1 = clause.list[f]
@@ -37,7 +37,7 @@ def manage_complementary(clauses):
                     found = True
                     break
             f = f + 1
-    for i in removable:
+    for i in reversed(removable):
         clauses.pop(i)
 
 def manage_bottoms(clauses):
@@ -46,10 +46,10 @@ def manage_bottoms(clauses):
         clause.remove_every(Formula("F"))
 
 def manage_copies(clauses):
-    """Remove from every clause repetion of inner formulas."""
+    """Remove from every clause repetions of inner formulas."""
     for clause in clauses:
         f = 0
-        while f < len(clause.list):
+        while f < len(clause.list)-1:
             formula = clause.list[f]
             f2 = f+1
             while f2 < len(clause.list):
@@ -58,6 +58,7 @@ def manage_copies(clauses):
                     clause.list.pop(f2)
                 else:
                     f2 = f2+1
+            f = f+1
 
 
 def is_closed(expansion):
diff --git a/pylogic/tests/test_propositional_resolution.py b/pylogic/tests/test_propositional_resolution.py
index 61a2631..3f2c724 100644
--- a/pylogic/tests/test_propositional_resolution.py
+++ b/pylogic/tests/test_propositional_resolution.py
@@ -8,6 +8,8 @@ class TestResolution(unittest.TestCase):
     def setUp(self):
         self.a1 = Formula("X")
         self.a2 = Formula("Y")
+        self.top = Formula("T")
+        self.bottom = Formula("F")
         self.l1 = Formula("!", Formula("X"))
         self.fand1 = Formula("&", Formula("X"), Formula("Y"))
         self.for1 = Formula("|", Formula("X"), Formula("Y"))
@@ -17,6 +19,75 @@ def setUp(self):
         self.taut4 = parser.parse("(P->(Q->R))->((P->Q)->(P->R))")
 
 
+    def test_preliminary_steps(self):
+        clauses = [Generalization("or", [self.top, self.a1, self.a2]),
+                   Generalization("or", [self.a2, self.a1, self.l1]),
+                   Generalization("or", [self.a1, self.a2, self.bottom]),
+                   Generalization("or", [self.a1, self.a2, self.a1]),
+                   Generalization("or", [self.a1, self.a2])]
+        exp_clauses = [Generalization("or", [self.a1, self.a2]),
+                       Generalization("or", [self.a1, self.a2]),
+                       Generalization("or", [self.a1, self.a2])]
+        resolution.preliminary_steps(clauses)
+        self.assertEqual(exp_clauses, clauses)
+
+    def test_manage_tops(self):
+        clauses = [Generalization("or", [self.top, self.a1, self.a2])]
+        exp_clauses = []
+        resolution.manage_tops(clauses)
+        self.assertEqual(exp_clauses, clauses)
+
+        clauses = [Generalization("or", [self.top, self.a1, self.a2]),
+                   Generalization("or", [self.bottom, self.top, self.a2]),
+                   Generalization("or", [self.a1, self.a2, self.top]),
+                   Generalization("or", [self.a1, self.a2])]
+        exp_clauses = [Generalization("or", [self.a1, self.a2])]
+        resolution.manage_tops(clauses)
+        self.assertEqual(exp_clauses, clauses)
+
+
+    def test_manage_complementary(self):
+        clauses = [Generalization("or", [self.a1, self.top, self.l1])]
+        exp_clauses = []
+        resolution.manage_complementary(clauses)
+        self.assertEqual(exp_clauses, clauses)
+
+        clauses = [Generalization("or", [self.a1, self.top, self.l1]),
+                   Generalization("or", [self.a2, self.a1, self.l1]),
+                   Generalization("or", [self.l1, self.top, self.a1]),
+                   Generalization("or", [self.a1, self.a2])]
+        exp_clauses = [Generalization("or", [self.a1, self.a2])]
+        resolution.manage_complementary(clauses)
+        self.assertEqual(exp_clauses, clauses)
+
+
+    def test_manage_bottoms(self):
+        clauses = [Generalization("or", [self.bottom, self.a1, self.a2]),
+                   Generalization("or", [self.a1, self.bottom, self.a2]),
+                   Generalization("or", [self.a1, self.a2, self.bottom]),
+                   Generalization("or", [self.a1, self.a2])]
+        exp_clauses = [Generalization("or", [self.a1, self.a2]),
+                       Generalization("or", [self.a1, self.a2]),
+                       Generalization("or", [self.a1, self.a2]),
+                       Generalization("or", [self.a1, self.a2])]
+        resolution.manage_bottoms(clauses)
+        self.assertEqual(exp_clauses, clauses)
+
+
+    def test_manage_copies(self):
+        clauses = [Generalization("or", [self.a1, self.a1, self.a2]),
+                   Generalization("or", [self.a1, self.a2, self.a1]),
+                   Generalization("or", [self.a2, self.a1, self.a2, self.a1]),
+                   Generalization("or", [self.a1, self.a2])]
+        exp_clauses = [Generalization("or", [self.a1, self.a2]),
+                       Generalization("or", [self.a1, self.a2]),
+                       Generalization("or", [self.a2, self.a1]),
+                       Generalization("or", [self.a1, self.a2])]
+        resolution.manage_copies(clauses)
+
+        self.assertEqual(exp_clauses, clauses)
+
+
     def test_is_tautology(self):
         self.assertFalse(resolution.is_tautology(self.a1))
         self.assertFalse(resolution.is_tautology(self.l1))
@@ -40,17 +111,6 @@ def test_is_closed(self):
         self.assertTrue(resolution.is_closed(expansion2))
 
 
-    def test_expand(self):
-        expansion1 = [[False, Generalization("or", [self.a2, self.l1])],
-                      [False, Generalization("or", [self.fand1, self.a1])],
-                      [False, Generalization("or", [self.fand1, self.for1])]]
-        exp1 = [[True, Generalization("or", [self.a2, self.l1])],
-                [False, Generalization("or", [self.fand1, self.a1])],
-                [False, Generalization("or", [self.fand1, self.for1])],
-                [False, Generalization("or", [self.a2, self.fand1])]]
-        result = resolution.expand(expansion1)
-        self.assertTrue(result)
-        self.assertEqual(exp1, expansion1)
 
 
 if __name__ == '__main__':

From b9bcf9a11c6b25f02779cca6648c1acf3406c998 Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Sun, 8 Sep 2013 11:03:58 +0200
Subject: [PATCH 03/19] Update is_closed

---
 pylogic/propositional/resolution.py            | 3 +--
 pylogic/tests/test_propositional_resolution.py | 2 --
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/pylogic/propositional/resolution.py b/pylogic/propositional/resolution.py
index c8aa4dd..56d186b 100644
--- a/pylogic/propositional/resolution.py
+++ b/pylogic/propositional/resolution.py
@@ -64,8 +64,7 @@ def manage_copies(clauses):
 def is_closed(expansion):
     """Given a list of clauses, return True if it contains an empty clause,
     False otherwise"""
-    for el in expansion:
-        clause = el[1]
+    for clause in expansion:
         if len(clause.list) == 0:
             return True
         # else ignore it
diff --git a/pylogic/tests/test_propositional_resolution.py b/pylogic/tests/test_propositional_resolution.py
index 3f2c724..11529ab 100644
--- a/pylogic/tests/test_propositional_resolution.py
+++ b/pylogic/tests/test_propositional_resolution.py
@@ -102,11 +102,9 @@ def test_is_tautology(self):
     def test_is_closed(self):
         expansion1 = [Generalization("or", [self.a1, self.l1]),
                       Generalization("or", [self.a2])]
-        expansion1 = [[False, disj] for disj in expansion1]
         expansion2 = [Generalization("or", [self.a1, self.l1]),
                       Generalization("or", []),
                       Generalization("or", [self.a2])]
-        expansion2 = [[False, disj] for disj in expansion2]
         self.assertFalse(resolution.is_closed(expansion1))
         self.assertTrue(resolution.is_closed(expansion2))
 

From 92d18f1f9695283f92bb97c36442d95d1a1f3d60 Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Sun, 8 Sep 2013 13:23:51 +0200
Subject: [PATCH 04/19] Test resolution_rule

---
 pylogic/propositional/resolution.py            | 6 +++---
 pylogic/tests/test_propositional_resolution.py | 8 ++++++++
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/pylogic/propositional/resolution.py b/pylogic/propositional/resolution.py
index 56d186b..3bf99e1 100644
--- a/pylogic/propositional/resolution.py
+++ b/pylogic/propositional/resolution.py
@@ -76,12 +76,12 @@ def resolution_rule(clause1, clause2, formula):
     new_clause = copy.deepcopy(clause1)
     other = copy.deepcopy(clause2)
     new_clause.remove_every(formula)
-    other.remove_every(temp_formula)
+    other.remove_every(formula.complement())
     new_clause.list.extend(other.list)
     return new_clause
 
 
-def resolution_rule_exhaust(clause1, clause2):
+def resolution_rule_complete(clause1, clause2):
     """Apply the resolution rule to the given clauses
     for every possible inner formulas"""
     new_clauses = []
@@ -110,7 +110,7 @@ def is_tautology(formula):
     closed = is_closed(expansion)
     while not closed and not picker.is_empty():
         clauses = picker.pick()
-        new_clauses = resolution_rule_exhaust(clauses[0], clauses[1])
+        new_clauses = resolution_rule_complete(clauses[0], clauses[1])
         picker.update(expansion, new_clauses)
         expansion.extend(new_clauses)
         disjs = ""
diff --git a/pylogic/tests/test_propositional_resolution.py b/pylogic/tests/test_propositional_resolution.py
index 11529ab..8f163c1 100644
--- a/pylogic/tests/test_propositional_resolution.py
+++ b/pylogic/tests/test_propositional_resolution.py
@@ -88,6 +88,14 @@ def test_manage_copies(self):
         self.assertEqual(exp_clauses, clauses)
 
 
+    def test_resolution_rule(self):
+        cl1 = Generalization("or", [self.a2, self.l1, self.bottom])
+        cl2 = Generalization("or", [self.top, self.a1])
+        form = self.l1
+        exp_cl = Generalization("or", [self.a2, self.bottom, self.top])
+        self.assertEqual(exp_cl, resolution.resolution_rule(cl1, cl2, form))
+
+
     def test_is_tautology(self):
         self.assertFalse(resolution.is_tautology(self.a1))
         self.assertFalse(resolution.is_tautology(self.l1))

From d1e140d87b35b62c89648bacf1c932f8128cd497 Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Sun, 8 Sep 2013 15:04:56 +0200
Subject: [PATCH 05/19] Change resolution_rule_complete in
 apply_resolution_rule and test

Has been changed the logic behind this function, because there is no reason to apply the
resolution rule more than one time on the same pair of clauses.
This is because if the resolution rule can be applied for example two times, it means that
there are at least two distinct couple of complementary literals in the two clauses.
When the resolution rule is applied to one these complementary literals in the resulting
clause there will be the other two complementary literals so the clause can be removed
because it is a tautology. The same result is obtained when the resolution rule is applied
on the other couple of complementary literals.
This theory needs to be verified.
---
 pylogic/propositional/resolution.py           | 29 +++++++++++--------
 .../tests/test_propositional_resolution.py    | 20 +++++++++++++
 2 files changed, 37 insertions(+), 12 deletions(-)

diff --git a/pylogic/propositional/resolution.py b/pylogic/propositional/resolution.py
index 3bf99e1..e1b821b 100644
--- a/pylogic/propositional/resolution.py
+++ b/pylogic/propositional/resolution.py
@@ -81,18 +81,22 @@ def resolution_rule(clause1, clause2, formula):
     return new_clause
 
 
-def resolution_rule_complete(clause1, clause2):
-    """Apply the resolution rule to the given clauses
-    for every possible inner formulas"""
-    new_clauses = []
+def apply_resolution_rule(clause1, clause2):
+    """Apply the resolution rule to the given clauses"""
     for f in range(len(clause1.list)):
         formula = clause1.list[f]
         # check if exists a complement of formula
-        for nf in range(len(clause2.list)):
-            temp_formula = clause2.list[nf]
-            if formula == temp_formula.complement():
-                clause = resolution_rule(clause1, clause2, formula)
-                new_clauses.append(clause)
+        for f2 in range(len(clause2.list)):
+            formula2 = clause2.list[f2]
+            if formula == formula2.complement():
+                new_clause = resolution_rule(clause1, clause2, formula)
+                clauses = [new_clause]
+                manage_complementary(clauses)
+                manage_copies(clauses)
+                if clauses == []:
+                    return None
+                else:
+                    return new_clause
 
 
 def is_tautology(formula):
@@ -110,9 +114,10 @@ def is_tautology(formula):
     closed = is_closed(expansion)
     while not closed and not picker.is_empty():
         clauses = picker.pick()
-        new_clauses = resolution_rule_complete(clauses[0], clauses[1])
-        picker.update(expansion, new_clauses)
-        expansion.extend(new_clauses)
+        new_clause = apply_resolution_rule(clauses[0], clauses[1])
+        if new_clause != None:
+            picker.update(expansion, new_clause)
+            expansion.append(new_clause)
         disjs = ""
         for g in expansion:
             disjs = disjs + " " + g[1].__str__()
diff --git a/pylogic/tests/test_propositional_resolution.py b/pylogic/tests/test_propositional_resolution.py
index 8f163c1..de46973 100644
--- a/pylogic/tests/test_propositional_resolution.py
+++ b/pylogic/tests/test_propositional_resolution.py
@@ -8,9 +8,12 @@ class TestResolution(unittest.TestCase):
     def setUp(self):
         self.a1 = Formula("X")
         self.a2 = Formula("Y")
+        self.a3 = Formula("Z")
+        self.a4 = Formula("W")
         self.top = Formula("T")
         self.bottom = Formula("F")
         self.l1 = Formula("!", Formula("X"))
+        self.l2 = Formula("!", Formula("Y"))
         self.fand1 = Formula("&", Formula("X"), Formula("Y"))
         self.for1 = Formula("|", Formula("X"), Formula("Y"))
         self.taut1 = parser.parse("((P->Q)&(Q->R))->-(-R&P)")
@@ -96,6 +99,23 @@ def test_resolution_rule(self):
         self.assertEqual(exp_cl, resolution.resolution_rule(cl1, cl2, form))
 
 
+    def test_apply_resolution_rule(self):
+        cl1 = Generalization("or", [self.a2, self.l1, self.a3])
+        cl2 = Generalization("or", [self.a4, self.a1])
+        exp_cls = Generalization("or", [self.a2, self.a3, self.a4])
+        self.assertEqual(exp_cls, resolution.apply_resolution_rule(cl1, cl2))
+        # complementary litterals in the result clause
+        cl1 = Generalization("or", [self.a2, self.l1, self.a3])
+        cl2 = Generalization("or", [self.a4, self.a1, self.l2])
+        exp_cls = None
+        self.assertEqual(exp_cls, resolution.apply_resolution_rule(cl1, cl2))
+        # copied litterals in the result clause
+        cl1 = Generalization("or", [self.a2, self.l1, self.a3])
+        cl2 = Generalization("or", [self.a4, self.a1, self.a2])
+        exp_cls = Generalization("or", [self.a2, self.a3, self.a4])
+        self.assertEqual(exp_cls, resolution.apply_resolution_rule(cl1, cl2))
+
+
     def test_is_tautology(self):
         self.assertFalse(resolution.is_tautology(self.a1))
         self.assertFalse(resolution.is_tautology(self.l1))

From 3028c69b395da0a77d58717a615f140f556db466 Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Sun, 8 Sep 2013 16:12:44 +0200
Subject: [PATCH 06/19] Add __len__() function to Generalization

---
 pylogic/propositional/propositional_logic.py       |  4 ++++
 pylogic/propositional/resolution.py                | 14 +++++++-------
 .../test_propositional_propositional_logic.py      |  9 +++++++++
 3 files changed, 20 insertions(+), 7 deletions(-)

diff --git a/pylogic/propositional/propositional_logic.py b/pylogic/propositional/propositional_logic.py
index d51a1ed..84de63b 100644
--- a/pylogic/propositional/propositional_logic.py
+++ b/pylogic/propositional/propositional_logic.py
@@ -277,6 +277,10 @@ def __ne__(self, other):
         return not self.__eq__(other)
 
 
+    def __len__(self):
+        return len(self.list)
+
+
     def has_non_literal(self):
         """Check if in the list of formulas there are non-literal formulas."""
         if len(self.list) == 0:
diff --git a/pylogic/propositional/resolution.py b/pylogic/propositional/resolution.py
index e1b821b..b381398 100644
--- a/pylogic/propositional/resolution.py
+++ b/pylogic/propositional/resolution.py
@@ -28,9 +28,9 @@ def manage_complementary(clauses):
         clause = clauses[c]
         found = False
         f = 0
-        while not found and f < len(clause.list):
+        while not found and f < len(clause):
             formula1 = clause.list[f]
-            for f2 in range(f+1, len(clause.list)):
+            for f2 in range(f+1, len(clause)):
                 formula2 = clause.list[f2]
                 if formula1 == formula2.complement():
                     removable.append(c)
@@ -49,10 +49,10 @@ def manage_copies(clauses):
     """Remove from every clause repetions of inner formulas."""
     for clause in clauses:
         f = 0
-        while f < len(clause.list)-1:
+        while f < len(clause)-1:
             formula = clause.list[f]
             f2 = f+1
-            while f2 < len(clause.list):
+            while f2 < len(clause):
                 formula2 = clause.list[f2]
                 if formula == formula2:
                     clause.list.pop(f2)
@@ -65,7 +65,7 @@ def is_closed(expansion):
     """Given a list of clauses, return True if it contains an empty clause,
     False otherwise"""
     for clause in expansion:
-        if len(clause.list) == 0:
+        if len(clause) == 0:
             return True
         # else ignore it
     return False
@@ -83,10 +83,10 @@ def resolution_rule(clause1, clause2, formula):
 
 def apply_resolution_rule(clause1, clause2):
     """Apply the resolution rule to the given clauses"""
-    for f in range(len(clause1.list)):
+    for f in range(len(clause1)):
         formula = clause1.list[f]
         # check if exists a complement of formula
-        for f2 in range(len(clause2.list)):
+        for f2 in range(len(clause2)):
             formula2 = clause2.list[f2]
             if formula == formula2.complement():
                 new_clause = resolution_rule(clause1, clause2, formula)
diff --git a/pylogic/tests/test_propositional_propositional_logic.py b/pylogic/tests/test_propositional_propositional_logic.py
index 4e52cd3..ee351e4 100644
--- a/pylogic/tests/test_propositional_propositional_logic.py
+++ b/pylogic/tests/test_propositional_propositional_logic.py
@@ -336,6 +336,15 @@ def test_eq_ne(self):
         self.assertNotEqual(g3, g1)
 
 
+    def test_len(self):
+        g1 = Generalization("and", [self.f1, self.f2])
+        g2 = Generalization("and", [self.f1, self.f2, self.f1, self.f2])
+        g3 = Generalization("and", [])
+        self.assertEqual(2, len(g1))
+        self.assertEqual(4, len(g2))
+        self.assertEqual(0, len(g3))
+
+
     def test_has_non_literal(self):
         g1 = Generalization("and", [self.f1, Formula("Z"), self.f2])
         g2 = Generalization("or", [Formula("Z"), Formula("!", Formula("Y"))])

From 4ec1af7245222f14c359a5cde68e466c843a1da7 Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Sun, 8 Sep 2013 23:48:29 +0200
Subject: [PATCH 07/19] Implement ClausePicker

---
 pylogic/propositional/resolution.py           | 73 ++++++++++++++-----
 .../tests/test_propositional_resolution.py    | 22 ++++++
 2 files changed, 78 insertions(+), 17 deletions(-)

diff --git a/pylogic/propositional/resolution.py b/pylogic/propositional/resolution.py
index b381398..2b08626 100644
--- a/pylogic/propositional/resolution.py
+++ b/pylogic/propositional/resolution.py
@@ -97,6 +97,7 @@ def apply_resolution_rule(clause1, clause2):
                     return None
                 else:
                     return new_clause
+    return None
 
 
 def is_tautology(formula):
@@ -111,31 +112,69 @@ def is_tautology(formula):
     expansion = cnf.list
     preliminary_steps(expansion)
     picker = ClausePicker(expansion)
-    closed = is_closed(expansion)
-    while not closed and not picker.is_empty():
-        clauses = picker.pick()
-        new_clause = apply_resolution_rule(clauses[0], clauses[1])
-        if new_clause != None:
-            picker.update(expansion, new_clause)
+    if is_closed(expansion):
+        return True
+    while not picker.is_empty():
+        cl = picker.pick()
+        new_clause = apply_resolution_rule(expansion[cl[0]], expansion[cl[1]])
+        if new_clause is not None:
+            if len(new_clause) == 0:
+                return True
+            picker.add_clause(new_clause)
             expansion.append(new_clause)
-        disjs = ""
-        for g in expansion:
-            disjs = disjs + " " + g[1].__str__()
-        print(disjs)
-        closed = is_closed(expansion)
-    return is_closed(expansion)
+            disjs = ""
+            for g in expansion:
+                disjs = disjs + " " + g.__str__()
+            print(disjs)
+    return False
 
 
 
 class ClausePicker():
     def __init__(self, expansion):
-        pass
+        # list with a couple (<size>, <index in espansion>) for each clause
+        self.db = [(len(clause), i) for i, clause in enumerate(expansion)]
+        self.db.sort()
+        # list where every entry is a couple of clauses indexes
+        # on which apply the resolution rule
+        self.couples = [(cl1, cl2)
+                        for (size, cl1) in self.db
+                        for (size2, cl2) in self.db if cl2 != cl1]
+
 
     def pick(self):
-        return None
+        if self.is_empty():
+            raise Exception("No more choices")
+        return self.couples.pop(0)
+
+
+    def add_clause(self, clause):
+        ex_index = len(self.db) # index in the expansion list
+        db_entry = (len(clause), ex_index)
+        # insert in self.db
+        self.db.append(db_entry)
+        self.db.sort()
+        db_ind = self.db.index(db_entry) # index in the list self.db
+        # insert in self.couples
+        new_c = [(ex_index, cl2) for (size2, cl2) in self.db if cl2 != ex_index]
+        if db_ind + 1 == len(self.db):
+            # append in the end of self.couples
+            self.couples.extend(new_c)
+        else:
+            # insert at a specific index of self.couples
+            (succ_size, succ_ex_ind) = self.db[db_ind+1]
+            # find the index of the successive in self.couples
+            found = False
+            succ_ind = 0
+            while not found and succ_ind < len(self.couples):
+                (ind1, ind2) = self.couples[succ_ind]
+                if (ind1 == succ_ex_ind):
+                    found = True
+                    succ_ind = succ_ind - 1
+                succ_ind = succ_ind + 1
+            pos = succ_ind
+            self.couples = self.couples[:pos] + new_c + self.couples[pos:]
 
-    def add_clause(self, expansion, clause):
-        pass
 
     def is_empty(self):
-        pass
+        return len(self.couples) == 0
diff --git a/pylogic/tests/test_propositional_resolution.py b/pylogic/tests/test_propositional_resolution.py
index de46973..34a5663 100644
--- a/pylogic/tests/test_propositional_resolution.py
+++ b/pylogic/tests/test_propositional_resolution.py
@@ -1,5 +1,6 @@
 import unittest
 from pylogic.propositional.propositional_logic import Formula, Generalization
+from pylogic.propositional.resolution import ClausePicker
 from pylogic.propositional import resolution
 from pylogic.propositional import parser
 
@@ -20,6 +21,7 @@ def setUp(self):
         self.taut2 = parser.parse("(-P->Q)->((P->Q)->Q)")
         self.taut3 = parser.parse("((P->Q)->P)->P")
         self.taut4 = parser.parse("(P->(Q->R))->((P->Q)->(P->R))")
+        self.taut5 = parser.parse("(F->X)")
 
 
     def test_preliminary_steps(self):
@@ -125,6 +127,7 @@ def test_is_tautology(self):
         self.assertTrue(resolution.is_tautology(self.taut2))
         self.assertTrue(resolution.is_tautology(self.taut3))
         self.assertTrue(resolution.is_tautology(self.taut4))
+        self.assertTrue(resolution.is_tautology(self.taut5))
 
 
     def test_is_closed(self):
@@ -138,6 +141,25 @@ def test_is_closed(self):
 
 
 
+class TestClausePicker(unittest.TestCase):
+    def setUp(self):
+        self.a1 = Formula("X")
+        self.a2 = Formula("Y")
+        self.a3 = Formula("Z")
+        self.a4 = Formula("W")
+        self.l1 = Formula("!", Formula("X"))
+
+
+    def test_init(self):
+        expansion = [Generalization("or", [self.a1, self.a3, self.l1]),
+                     Generalization("or", [self.a2, self.l1]),
+                     Generalization("or", [self.l1, self.a4, self.a1]),
+                     Generalization("or", [self.a3])]
+        cp = ClausePicker(expansion)
+        exp_db = [(1, 3), (2, 1), (3, 0), (3, 2)]
+        self.assertEqual(exp_db, cp.db)
+
+
 
 if __name__ == '__main__':
     unittest.main()

From dd975316e776f2c872bd6f19b475c53df58e6c82 Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Tue, 10 Sep 2013 13:33:09 +0200
Subject: [PATCH 08/19] Add execution time in gui

---
 pylogic/gui/gui.py        | 22 +++++++++++++++++++---
 pylogic/gui/mainwindow.ui | 13 +++++++++++++
 2 files changed, 32 insertions(+), 3 deletions(-)

diff --git a/pylogic/gui/gui.py b/pylogic/gui/gui.py
index b6107bf..0eefff2 100755
--- a/pylogic/gui/gui.py
+++ b/pylogic/gui/gui.py
@@ -1,6 +1,7 @@
 import sys
 import string
 import os.path  # for file checks
+import time
 
 from PyQt4.QtCore import Qt, SIGNAL
 from PyQt4.QtGui import *
@@ -30,6 +31,18 @@ def appendOutput(self, string=""):
         outputBox.write(string)
 
 
+    def execute(self, func):
+         check_box = self.ui.checkBoxExecutionTime.isChecked()
+         start = 0
+         if check_box:
+             start = time.time()
+         output = func()
+         if check_box:
+             execution_time = time.time() - start
+             self.appendOutput("Execution time: " + execution_time.__str__())
+         return output
+
+
     def showAboutBox(self):
         aboutBox = MyAboutBox()
         aboutBox.setModal(False)
@@ -67,20 +80,23 @@ def propositionalCheck(self):
     def propositionalNNF(self):
         """Transform the current formula in input in NNF"""
         formula = propositional_parser.parse(self.getInputString())
-        output = formula.nnf()
+        func = lambda: formula.nnf()
+        output = self.execute(func)
         self.appendOutput(output.__str__())
 
     def propositionalCNF(self):
         """Transform the current formula in input in CNF"""
         formula = propositional_parser.parse(self.getInputString())
-        output = formula.cnf()
+        func = lambda: formula.cnf()
+        output = self.execute(func)
         self.appendOutput(output.__str__())
 
     def propositionalResolution(self):
         """Test if the current formula is a tautology, using the resolution
         method"""
         formula = propositional_parser.parse(self.getInputString())
-        output = propositional_resolution.is_tautology(formula)
+        func = lambda: propositional_resolution.is_tautology(formula)
+        output = self.execute(func)
         self.appendOutput("%s: %s" % (str(formula), output.__str__()) )
 
 
diff --git a/pylogic/gui/mainwindow.ui b/pylogic/gui/mainwindow.ui
index 5862ffb..4bd7123 100644
--- a/pylogic/gui/mainwindow.ui
+++ b/pylogic/gui/mainwindow.ui
@@ -158,6 +158,19 @@
            </property>
           </spacer>
          </item>
+         <item>
+          <widget class="QCheckBox" name="checkBoxExecutionTime">
+           <property name="enabled">
+            <bool>true</bool>
+           </property>
+           <property name="text">
+            <string>execution time</string>
+           </property>
+           <property name="checked">
+            <bool>true</bool>
+           </property>
+          </widget>
+         </item>
         </layout>
        </widget>
        <widget class="QWidget" name="tabFirstOrder">

From 51f538e5f39434e699ddf0ed47854ce4900c9d01 Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Wed, 11 Sep 2013 00:07:13 +0200
Subject: [PATCH 09/19] In Generalization add equality test order independent

---
 pylogic/propositional/propositional_logic.py       | 14 ++++++++++++++
 .../test_propositional_propositional_logic.py      |  8 ++++++++
 2 files changed, 22 insertions(+)

diff --git a/pylogic/propositional/propositional_logic.py b/pylogic/propositional/propositional_logic.py
index 84de63b..265dc02 100644
--- a/pylogic/propositional/propositional_logic.py
+++ b/pylogic/propositional/propositional_logic.py
@@ -281,6 +281,20 @@ def __len__(self):
         return len(self.list)
 
 
+    def equivalent(self, other):
+        """Check if two generalizations have the same elements independently of
+        their order"""
+        if len(self.list) != len(other.list):
+            return False
+        other_list = list(other.list)
+        try:
+            for formula in self.list:
+                other_list.remove(formula)
+        except ValueError:
+            return False
+        return not other_list
+
+
     def has_non_literal(self):
         """Check if in the list of formulas there are non-literal formulas."""
         if len(self.list) == 0:
diff --git a/pylogic/tests/test_propositional_propositional_logic.py b/pylogic/tests/test_propositional_propositional_logic.py
index ee351e4..b56e524 100644
--- a/pylogic/tests/test_propositional_propositional_logic.py
+++ b/pylogic/tests/test_propositional_propositional_logic.py
@@ -345,6 +345,14 @@ def test_len(self):
         self.assertEqual(0, len(g3))
 
 
+    def test_equivalent(self):
+        g1 = Generalization("and", [self.f1, self.f2])
+        g2 = Generalization("and", [self.f2, self.f1])
+        g3 = Generalization("and", [self.f1])
+        self.assertTrue(g1.equivalent(g2))
+        self.assertFalse(g1.equivalent(g3))
+
+
     def test_has_non_literal(self):
         g1 = Generalization("and", [self.f1, Formula("Z"), self.f2])
         g2 = Generalization("or", [Formula("Z"), Formula("!", Formula("Y"))])

From b8c9aeb2e43fc41ceadc1c9e93ddf878b2fcbd53 Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Wed, 11 Sep 2013 00:19:38 +0200
Subject: [PATCH 10/19] Don't expand with a clause already present

---
 pylogic/propositional/resolution.py           | 22 ++++++++++++++-----
 .../tests/test_propositional_resolution.py    | 12 ++++++++++
 2 files changed, 28 insertions(+), 6 deletions(-)

diff --git a/pylogic/propositional/resolution.py b/pylogic/propositional/resolution.py
index 2b08626..f1122a6 100644
--- a/pylogic/propositional/resolution.py
+++ b/pylogic/propositional/resolution.py
@@ -71,6 +71,18 @@ def is_closed(expansion):
     return False
 
 
+def is_new(expansion, clause):
+    """Check if the given clause is already present in the given expansion."""
+    found = False
+    i = 0
+    while not found and i < len(expansion):
+        cl = expansion[i]
+        i = i + 1
+        if cl.equivalent(clause):
+            return False
+    return True
+
+
 def resolution_rule(clause1, clause2, formula):
     """Apply the resolution rule to the given clauses and formula."""
     new_clause = copy.deepcopy(clause1)
@@ -120,12 +132,10 @@ def is_tautology(formula):
         if new_clause is not None:
             if len(new_clause) == 0:
                 return True
-            picker.add_clause(new_clause)
-            expansion.append(new_clause)
-            disjs = ""
-            for g in expansion:
-                disjs = disjs + " " + g.__str__()
-            print(disjs)
+            if is_new(expansion, new_clause):
+                expansion.append(new_clause)
+                picker.add_clause(new_clause)
+                print(" ".join([cl.__str__() for cl in expansion]))
     return False
 
 
diff --git a/pylogic/tests/test_propositional_resolution.py b/pylogic/tests/test_propositional_resolution.py
index 34a5663..47c7ce9 100644
--- a/pylogic/tests/test_propositional_resolution.py
+++ b/pylogic/tests/test_propositional_resolution.py
@@ -140,6 +140,18 @@ def test_is_closed(self):
         self.assertTrue(resolution.is_closed(expansion2))
 
 
+    def test_is_new(self):
+        expansion1 = [Generalization("or", [self.a1, self.l1]),
+                      Generalization("or", [self.a2])]
+        gen1 = Generalization("or", [self.l1, self.a1])
+        self.assertFalse(resolution.is_new(expansion1, gen1))
+        expansion2 = [Generalization("or", [self.a1, self.l1]),
+                      Generalization("or", []),
+                      Generalization("or", [self.a2])]
+        gen2 = Generalization("or", [self.l1])
+        self.assertTrue(resolution.is_new(expansion2, gen2))
+
+
 
 class TestClausePicker(unittest.TestCase):
     def setUp(self):

From 4ea779930f68e3893cbde0d8c02f0424460c80dd Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Wed, 11 Sep 2013 00:21:33 +0200
Subject: [PATCH 11/19] Fix equality test in Generalization

---
 pylogic/propositional/propositional_logic.py            | 2 ++
 pylogic/tests/test_propositional_propositional_logic.py | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/pylogic/propositional/propositional_logic.py b/pylogic/propositional/propositional_logic.py
index 265dc02..0782110 100644
--- a/pylogic/propositional/propositional_logic.py
+++ b/pylogic/propositional/propositional_logic.py
@@ -284,6 +284,8 @@ def __len__(self):
     def equivalent(self, other):
         """Check if two generalizations have the same elements independently of
         their order"""
+        if self.connective != other.connective:
+            return False
         if len(self.list) != len(other.list):
             return False
         other_list = list(other.list)
diff --git a/pylogic/tests/test_propositional_propositional_logic.py b/pylogic/tests/test_propositional_propositional_logic.py
index b56e524..dde49da 100644
--- a/pylogic/tests/test_propositional_propositional_logic.py
+++ b/pylogic/tests/test_propositional_propositional_logic.py
@@ -349,8 +349,10 @@ def test_equivalent(self):
         g1 = Generalization("and", [self.f1, self.f2])
         g2 = Generalization("and", [self.f2, self.f1])
         g3 = Generalization("and", [self.f1])
+        g4 = Generalization("or", [self.f2, self.f1])
         self.assertTrue(g1.equivalent(g2))
         self.assertFalse(g1.equivalent(g3))
+        self.assertFalse(g1.equivalent(g4))
 
 
     def test_has_non_literal(self):

From 5806a1c63f129a9d88f1ebc2631efbde20110e51 Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Wed, 11 Sep 2013 01:18:31 +0200
Subject: [PATCH 12/19] Improve the heuristic short clauses first

Sort the couples of clauses with the sum of the sizes.
With this has been saved one forth of execution time.
---
 pylogic/propositional/resolution.py           | 64 +++++++++----------
 .../tests/test_propositional_resolution.py    |  9 ++-
 2 files changed, 36 insertions(+), 37 deletions(-)

diff --git a/pylogic/propositional/resolution.py b/pylogic/propositional/resolution.py
index f1122a6..4523166 100644
--- a/pylogic/propositional/resolution.py
+++ b/pylogic/propositional/resolution.py
@@ -142,49 +142,43 @@ def is_tautology(formula):
 
 class ClausePicker():
     def __init__(self, expansion):
-        # list with a couple (<size>, <index in espansion>) for each clause
-        self.db = [(len(clause), i) for i, clause in enumerate(expansion)]
-        self.db.sort()
-        # list where every entry is a couple of clauses indexes
-        # on which apply the resolution rule
-        self.couples = [(cl1, cl2)
-                        for (size, cl1) in self.db
-                        for (size2, cl2) in self.db if cl2 != cl1]
+        self.sizes = [len(clause) for clause in expansion]
+        # dict containing the couples of clauses (their indexes)
+        # it is indexed with the sum of the two clauses' sizes
+        self.buckets = dict()
+        for i in range(len(self.sizes)-1):
+            size_i = self.sizes[i]
+            for j in range(i+1, len(self.sizes)):
+                size = size_i + self.sizes[j]
+                if size in self.buckets:
+                    self.buckets[size].append((i,j))
+                else:
+                    self.buckets[size] = [(i,j)]
 
 
     def pick(self):
         if self.is_empty():
             raise Exception("No more choices")
-        return self.couples.pop(0)
+        bucket = min(self.buckets.keys())
+        couple = self.buckets[bucket].pop(0)
+        if len(self.buckets[bucket]) == 0:
+            del self.buckets[bucket]
+        return couple
 
 
     def add_clause(self, clause):
-        ex_index = len(self.db) # index in the expansion list
-        db_entry = (len(clause), ex_index)
-        # insert in self.db
-        self.db.append(db_entry)
-        self.db.sort()
-        db_ind = self.db.index(db_entry) # index in the list self.db
-        # insert in self.couples
-        new_c = [(ex_index, cl2) for (size2, cl2) in self.db if cl2 != ex_index]
-        if db_ind + 1 == len(self.db):
-            # append in the end of self.couples
-            self.couples.extend(new_c)
-        else:
-            # insert at a specific index of self.couples
-            (succ_size, succ_ex_ind) = self.db[db_ind+1]
-            # find the index of the successive in self.couples
-            found = False
-            succ_ind = 0
-            while not found and succ_ind < len(self.couples):
-                (ind1, ind2) = self.couples[succ_ind]
-                if (ind1 == succ_ex_ind):
-                    found = True
-                    succ_ind = succ_ind - 1
-                succ_ind = succ_ind + 1
-            pos = succ_ind
-            self.couples = self.couples[:pos] + new_c + self.couples[pos:]
+        i = len(self.sizes) # index in the expansion list
+        # insert in self.sizes
+        size_i = len(clause)
+        self.sizes.append(size_i)
+        # insert in self.buckets
+        for j in range(len(self.sizes)-1):
+                size = size_i + self.sizes[j]
+                if size in self.buckets:
+                    self.buckets[size].append((i,j))
+                else:
+                    self.buckets[size] = [(i,j)]
 
 
     def is_empty(self):
-        return len(self.couples) == 0
+        return len(self.buckets) == 0
diff --git a/pylogic/tests/test_propositional_resolution.py b/pylogic/tests/test_propositional_resolution.py
index 47c7ce9..decdfde 100644
--- a/pylogic/tests/test_propositional_resolution.py
+++ b/pylogic/tests/test_propositional_resolution.py
@@ -168,8 +168,13 @@ def test_init(self):
                      Generalization("or", [self.l1, self.a4, self.a1]),
                      Generalization("or", [self.a3])]
         cp = ClausePicker(expansion)
-        exp_db = [(1, 3), (2, 1), (3, 0), (3, 2)]
-        self.assertEqual(exp_db, cp.db)
+        exp_sizes = [3, 2, 3, 1]
+        self.assertEqual(exp_sizes, cp.sizes)
+        exp_buckets = {3: [(1, 3)],
+                       4: [(0, 3), (2, 3)],
+                       5: [(0, 1), (1, 2)],
+                       6: [(0, 2)]}
+        self.assertEqual(exp_buckets, cp.buckets)
 
 
 

From f028e18994788bb4be67829181a5ab4e00ccbf95 Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Sat, 14 Sep 2013 16:11:11 +0200
Subject: [PATCH 13/19] Test ClausePicker

---
 pylogic/propositional/resolution.py           |  19 ++-
 .../tests/test_propositional_resolution.py    | 115 +++++++++++++-----
 2 files changed, 100 insertions(+), 34 deletions(-)

diff --git a/pylogic/propositional/resolution.py b/pylogic/propositional/resolution.py
index 4523166..df882da 100644
--- a/pylogic/propositional/resolution.py
+++ b/pylogic/propositional/resolution.py
@@ -94,7 +94,21 @@ def resolution_rule(clause1, clause2, formula):
 
 
 def apply_resolution_rule(clause1, clause2):
-    """Apply the resolution rule to the given clauses"""
+    """Apply the resolution rule to the given clauses.
+
+    After that apply the preliminary steps on the resulting clause.
+    It assumes that in clause1 and clause2 are already applied
+    the preliminary steps, that is in them there aren't tops or bottoms;
+    so here are not applied manage_tops or manage_bottoms.
+
+    Moreover the resolution rule is applied only on the first formula
+    of which is found the complementary in the other clause.
+    This because if the resolution rule could be applied, for instance,
+    two times it means that in them there are two distinct couples
+    of complementary formulas, this means that after every application
+    of the resolution rule in the resulting clauses there will be
+    a couple of complementary fomulas and so with the preliminary steps
+    the clauses will be removed."""
     for f in range(len(clause1)):
         formula = clause1.list[f]
         # check if exists a complement of formula
@@ -143,7 +157,8 @@ def is_tautology(formula):
 class ClausePicker():
     def __init__(self, expansion):
         self.sizes = [len(clause) for clause in expansion]
-        # dict containing the couples of clauses (their indexes)
+        # dict containing the couples of clauses
+        # (precisely their indexes in the original expansion list)
         # it is indexed with the sum of the two clauses' sizes
         self.buckets = dict()
         for i in range(len(self.sizes)-1):
diff --git a/pylogic/tests/test_propositional_resolution.py b/pylogic/tests/test_propositional_resolution.py
index decdfde..7b4592d 100644
--- a/pylogic/tests/test_propositional_resolution.py
+++ b/pylogic/tests/test_propositional_resolution.py
@@ -1,4 +1,5 @@
 import unittest
+import copy
 from pylogic.propositional.propositional_logic import Formula, Generalization
 from pylogic.propositional.resolution import ClausePicker
 from pylogic.propositional import resolution
@@ -93,6 +94,28 @@ def test_manage_copies(self):
         self.assertEqual(exp_clauses, clauses)
 
 
+    def test_is_closed(self):
+        expansion1 = [Generalization("or", [self.a1, self.l1]),
+                      Generalization("or", [self.a2])]
+        expansion2 = [Generalization("or", [self.a1, self.l1]),
+                      Generalization("or", []),
+                      Generalization("or", [self.a2])]
+        self.assertFalse(resolution.is_closed(expansion1))
+        self.assertTrue(resolution.is_closed(expansion2))
+
+
+    def test_is_new(self):
+        expansion1 = [Generalization("or", [self.a1, self.l1]),
+                      Generalization("or", [self.a2])]
+        gen1 = Generalization("or", [self.l1, self.a1])
+        self.assertFalse(resolution.is_new(expansion1, gen1))
+        expansion2 = [Generalization("or", [self.a1, self.l1]),
+                      Generalization("or", []),
+                      Generalization("or", [self.a2])]
+        gen2 = Generalization("or", [self.l1])
+        self.assertTrue(resolution.is_new(expansion2, gen2))
+
+
     def test_resolution_rule(self):
         cl1 = Generalization("or", [self.a2, self.l1, self.bottom])
         cl2 = Generalization("or", [self.top, self.a1])
@@ -116,6 +139,11 @@ def test_apply_resolution_rule(self):
         cl2 = Generalization("or", [self.a4, self.a1, self.a2])
         exp_cls = Generalization("or", [self.a2, self.a3, self.a4])
         self.assertEqual(exp_cls, resolution.apply_resolution_rule(cl1, cl2))
+        # no complementary formulas in the clauses
+        cl1 = Generalization("or", [self.a2, self.a4, self.a3])
+        cl2 = Generalization("or", [self.a4, self.a1, self.a3])
+        exp_cls = None
+        self.assertEqual(exp_cls, resolution.apply_resolution_rule(cl1, cl2))
 
 
     def test_is_tautology(self):
@@ -130,28 +158,6 @@ def test_is_tautology(self):
         self.assertTrue(resolution.is_tautology(self.taut5))
 
 
-    def test_is_closed(self):
-        expansion1 = [Generalization("or", [self.a1, self.l1]),
-                      Generalization("or", [self.a2])]
-        expansion2 = [Generalization("or", [self.a1, self.l1]),
-                      Generalization("or", []),
-                      Generalization("or", [self.a2])]
-        self.assertFalse(resolution.is_closed(expansion1))
-        self.assertTrue(resolution.is_closed(expansion2))
-
-
-    def test_is_new(self):
-        expansion1 = [Generalization("or", [self.a1, self.l1]),
-                      Generalization("or", [self.a2])]
-        gen1 = Generalization("or", [self.l1, self.a1])
-        self.assertFalse(resolution.is_new(expansion1, gen1))
-        expansion2 = [Generalization("or", [self.a1, self.l1]),
-                      Generalization("or", []),
-                      Generalization("or", [self.a2])]
-        gen2 = Generalization("or", [self.l1])
-        self.assertTrue(resolution.is_new(expansion2, gen2))
-
-
 
 class TestClausePicker(unittest.TestCase):
     def setUp(self):
@@ -160,23 +166,68 @@ def setUp(self):
         self.a3 = Formula("Z")
         self.a4 = Formula("W")
         self.l1 = Formula("!", Formula("X"))
+        self.expansion = [Generalization("or", [self.a1, self.l1, self.a3]),
+                          Generalization("or", [self.a2, self.l1]),
+                          Generalization("or", [self.l1, self.a1, self.a4]),
+                          Generalization("or", [self.a3])]
+        self.sizes = [3, 2, 3, 1]
+        self.buckets = {3: [(1, 3)],
+                        4: [(0, 3), (2, 3)],
+                        5: [(0, 1), (1, 2)],
+                        6: [(0, 2)]}
 
 
     def test_init(self):
-        expansion = [Generalization("or", [self.a1, self.a3, self.l1]),
-                     Generalization("or", [self.a2, self.l1]),
-                     Generalization("or", [self.l1, self.a4, self.a1]),
-                     Generalization("or", [self.a3])]
-        cp = ClausePicker(expansion)
-        exp_sizes = [3, 2, 3, 1]
+        cp = ClausePicker(self.expansion)
+        self.assertEqual(self.sizes, cp.sizes)
+        self.assertEqual(self.buckets, cp.buckets)
+
+
+    def test_pick(self):
+        cp = ClausePicker(self.expansion)
+        self.assertEqual((1, 3), cp.pick())
+        self.assertEqual((0, 3), cp.pick())
+        self.assertEqual((2, 3), cp.pick())
+        self.assertEqual((0, 1), cp.pick())
+        self.assertEqual((1, 2), cp.pick())
+        self.assertEqual((0, 2), cp.pick())
+        # empty buckets
+        self.assertRaises(Exception, cp.pick)
+
+
+    def test_add_clause(self):
+        cp = ClausePicker(self.expansion)
+        gen = Generalization("or", [self.a1, self.a2, self.a3, self.a4])
+        cp.add_clause(gen)
+        exp_sizes = list(self.sizes)
+        exp_sizes.append(len(gen))
         self.assertEqual(exp_sizes, cp.sizes)
-        exp_buckets = {3: [(1, 3)],
-                       4: [(0, 3), (2, 3)],
-                       5: [(0, 1), (1, 2)],
-                       6: [(0, 2)]}
+        exp_buckets = copy.deepcopy(self.buckets)
+        new_index = 4
+        exp_buckets[7] = [(new_index, 0)]
+        exp_buckets[6].append((new_index, 1))
+        exp_buckets[7].append((new_index, 2))
+        exp_buckets[5].append((new_index, 3))
         self.assertEqual(exp_buckets, cp.buckets)
 
 
+    def test_is_empty(self):
+        cp = ClausePicker(self.expansion)
+        self.assertFalse(cp.is_empty())
+        cp.pick()
+        self.assertFalse(cp.is_empty())
+        cp.pick()
+        self.assertFalse(cp.is_empty())
+        cp.pick()
+        self.assertFalse(cp.is_empty())
+        cp.pick()
+        self.assertFalse(cp.is_empty())
+        cp.pick()
+        self.assertFalse(cp.is_empty())
+        cp.pick()
+        self.assertTrue(cp.is_empty())
+
+
 
 if __name__ == '__main__':
     unittest.main()

From c46b62dac3e2ce61f2d315f3477c7a2a7ba58b49 Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Sat, 14 Sep 2013 18:24:32 +0200
Subject: [PATCH 14/19] Test resolution with many tautologies

---
 examples/prop_satisfiables.txt                |  4 ++
 examples/prop_tautologies.txt                 | 46 +++++++++++++++++++
 .../tests/test_propositional_resolution.py    | 20 ++++----
 3 files changed, 61 insertions(+), 9 deletions(-)
 create mode 100644 examples/prop_satisfiables.txt
 create mode 100644 examples/prop_tautologies.txt

diff --git a/examples/prop_satisfiables.txt b/examples/prop_satisfiables.txt
new file mode 100644
index 0000000..1b89fd2
--- /dev/null
+++ b/examples/prop_satisfiables.txt
@@ -0,0 +1,4 @@
+X
+Y
+X&Y
+X|Y
diff --git a/examples/prop_tautologies.txt b/examples/prop_tautologies.txt
new file mode 100644
index 0000000..2c67d66
--- /dev/null
+++ b/examples/prop_tautologies.txt
@@ -0,0 +1,46 @@
+%% Tautologies from:
+%%   Melvin Fitting. "First-Order Logic and Automated Theorem Proving".
+
+%% from Tableaux exercises
+((P -> Q) & (Q -> R)) -> -(-R & P)
+(-P -> Q) -> ((P -> Q) -> Q)
+((P -> Q) -> P) -> P
+-(-(P & P) & P)
+--(-(P | Q) | (P | Q))
+-(-P | -Q) <- --(P & Q)
+((((A -> B) -> (-C -> -D)) -> C) -> E) -> ((E -> A) -> (D -> A))
+-(-(P & -(Q & R)) & -(-(P & -(R & P)) & -(-(S & Q) & -(-(P & S) & -(P & S)))))
+-(-(P & -(Q & R)) & -(-(-(S & R) & -(-(P & S) & -(P & S))) & -(P & -(P & Q))))
+
+%% from Resolution example
+((P & Q) | (R -> S)) -> ((P | (R -> S)) & (Q | (R -> S)))
+
+%% Hilbert System Axioms
+X -> (Y -> X)
+(X -> (Y -> Z)) -> ((X -> Y) -> (X -> Z))
+F -> X
+X -> T
+--X -> X
+X -> (-X -> Y)
+% axiom scheme 7 application
+(A & B) -> A
+% axiom scheme 8 application
+(A & B) -> B
+% axiom scheme 9 application
+(A -> X) -> ((B -> X) -> ((A | B) -> X))
+
+%% from Natural Deduction exercises
+% X -> (Y -> X)
+(X -> (Y -> Z)) -> ((X -> Y) -> (X -> Z))
+(-Y -> -X) -> ((-Y -> X) -> Y)
+% ((X -> Y) -> X) -> X
+(X & (Y | Z)) -> ((X & Y) | (X & Z))
+(X -> Y) -> (-(Y | Z) -> -(X | Z))
+-(-(P & P) & P)
+--(-(P | Q) | (P | Q))
+-(-P | -Q) <- --(P & Q)
+
+%% from Davis-Putnam exercises
+((P -> Q) -> (P -> R)) -> (P -> (Q -> R))
+(P & Q) <-> -(-P | -Q)
+(P -> Q) | (Q -> R)
diff --git a/pylogic/tests/test_propositional_resolution.py b/pylogic/tests/test_propositional_resolution.py
index 7b4592d..3616528 100644
--- a/pylogic/tests/test_propositional_resolution.py
+++ b/pylogic/tests/test_propositional_resolution.py
@@ -147,15 +147,17 @@ def test_apply_resolution_rule(self):
 
 
     def test_is_tautology(self):
-        self.assertFalse(resolution.is_tautology(self.a1))
-        self.assertFalse(resolution.is_tautology(self.l1))
-        self.assertFalse(resolution.is_tautology(self.fand1))
-        self.assertFalse(resolution.is_tautology(self.for1))
-        self.assertTrue(resolution.is_tautology(self.taut1))
-        self.assertTrue(resolution.is_tautology(self.taut2))
-        self.assertTrue(resolution.is_tautology(self.taut3))
-        self.assertTrue(resolution.is_tautology(self.taut4))
-        self.assertTrue(resolution.is_tautology(self.taut5))
+        def test(filename, truth):
+            f = open(filename, "r")
+            for formula_s in f:
+                if len(formula_s) > 0 and formula_s[0] not in ["%", "\n"]:
+                    formula = parser.parse(formula_s)
+                    self.assertEqual(truth, resolution.is_tautology(formula))
+
+        tautologies_fn = "examples/prop_tautologies.txt"
+        test(tautologies_fn, True)
+        satisfiables_fn = "examples/prop_satisfiables.txt"
+        test(satisfiables_fn, False)
 
 
 

From 5f94b87ce88032845c60e271cf5f15b3927f7eec Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Sat, 14 Sep 2013 19:19:46 +0200
Subject: [PATCH 15/19] Remove duplicated clauses before resolution

---
 pylogic/propositional/resolution.py           | 20 +++++++++++++++++++
 .../tests/test_propositional_resolution.py    | 18 +++++++++++++----
 2 files changed, 34 insertions(+), 4 deletions(-)

diff --git a/pylogic/propositional/resolution.py b/pylogic/propositional/resolution.py
index df882da..ec83a2b 100644
--- a/pylogic/propositional/resolution.py
+++ b/pylogic/propositional/resolution.py
@@ -8,6 +8,7 @@ def preliminary_steps(clauses):
     manage_complementary(clauses)
     manage_bottoms(clauses)
     manage_copies(clauses)
+    manage_duplicated_clauses(clauses)
 
 def manage_tops(clauses):
     """Remove the clauses containg the top."""
@@ -60,6 +61,25 @@ def manage_copies(clauses):
                     f2 = f2+1
             f = f+1
 
+def manage_duplicated_clauses(clauses):
+    """Remove duplicated clauses, independently of the order of the formulas."""
+    # old_clauses = copy.deepcopy(clauses)
+    # clauses = list()
+    # for clause in old_clauses:
+    #     if is_new(clauses, clause):
+    #         clauses.append(clause)
+    removable = []
+    for i in range(len(clauses)):
+        if i not in removable:
+            clause = clauses[i]
+            for j in range(i + 1, len(clauses)):
+                if j not in removable:
+                    clause2 = clauses[j]
+                    if clause.equivalent(clause2):
+                        removable.append(j)
+    for i in reversed(removable):
+        clauses.pop(i)
+
 
 def is_closed(expansion):
     """Given a list of clauses, return True if it contains an empty clause,
diff --git a/pylogic/tests/test_propositional_resolution.py b/pylogic/tests/test_propositional_resolution.py
index 3616528..5245a0a 100644
--- a/pylogic/tests/test_propositional_resolution.py
+++ b/pylogic/tests/test_propositional_resolution.py
@@ -29,11 +29,11 @@ def test_preliminary_steps(self):
         clauses = [Generalization("or", [self.top, self.a1, self.a2]),
                    Generalization("or", [self.a2, self.a1, self.l1]),
                    Generalization("or", [self.a1, self.a2, self.bottom]),
-                   Generalization("or", [self.a1, self.a2, self.a1]),
-                   Generalization("or", [self.a1, self.a2])]
+                   Generalization("or", [self.a1, self.a3, self.a1]),
+                   Generalization("or", [self.a1, self.a4])]
         exp_clauses = [Generalization("or", [self.a1, self.a2]),
-                       Generalization("or", [self.a1, self.a2]),
-                       Generalization("or", [self.a1, self.a2])]
+                       Generalization("or", [self.a1, self.a3]),
+                       Generalization("or", [self.a1, self.a4])]
         resolution.preliminary_steps(clauses)
         self.assertEqual(exp_clauses, clauses)
 
@@ -90,7 +90,17 @@ def test_manage_copies(self):
                        Generalization("or", [self.a2, self.a1]),
                        Generalization("or", [self.a1, self.a2])]
         resolution.manage_copies(clauses)
+        self.assertEqual(exp_clauses, clauses)
+
 
+    def test_manage_duplicated_clauses(self):
+        clauses = [Generalization("or", [self.a1, self.a2]),
+                   Generalization("or", [self.a2, self.l1, self.a1]),
+                   Generalization("or", [self.a2, self.a1]),
+                   Generalization("or", [self.a1, self.a2, self.l1])]
+        exp_clauses = [Generalization("or", [self.a1, self.a2]),
+                       Generalization("or", [self.a2, self.l1, self.a1])]
+        resolution.manage_duplicated_clauses(clauses)
         self.assertEqual(exp_clauses, clauses)
 
 

From ed3d36784e2e40e044e53fca66ab0a4331a88c6c Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Sun, 15 Sep 2013 12:10:47 +0200
Subject: [PATCH 16/19] Little clean up

---
 pylogic/propositional/resolution.py | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/pylogic/propositional/resolution.py b/pylogic/propositional/resolution.py
index ec83a2b..ebb6632 100644
--- a/pylogic/propositional/resolution.py
+++ b/pylogic/propositional/resolution.py
@@ -63,11 +63,6 @@ def manage_copies(clauses):
 
 def manage_duplicated_clauses(clauses):
     """Remove duplicated clauses, independently of the order of the formulas."""
-    # old_clauses = copy.deepcopy(clauses)
-    # clauses = list()
-    # for clause in old_clauses:
-    #     if is_new(clauses, clause):
-    #         clauses.append(clause)
     removable = []
     for i in range(len(clauses)):
         if i not in removable:

From 2af93d1723e45accbc847d8c59d55a68febfc295 Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Sun, 15 Sep 2013 15:24:08 +0200
Subject: [PATCH 17/19] Remove deepcopy from resolution_rule

Now resolution_rule takes almost 1/30 of the time
---
 pylogic/propositional/resolution.py | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/pylogic/propositional/resolution.py b/pylogic/propositional/resolution.py
index ebb6632..e9bf362 100644
--- a/pylogic/propositional/resolution.py
+++ b/pylogic/propositional/resolution.py
@@ -100,11 +100,15 @@ def is_new(expansion, clause):
 
 def resolution_rule(clause1, clause2, formula):
     """Apply the resolution rule to the given clauses and formula."""
-    new_clause = copy.deepcopy(clause1)
-    other = copy.deepcopy(clause2)
-    new_clause.remove_every(formula)
-    other.remove_every(formula.complement())
-    new_clause.list.extend(other.list)
+    new_clause = Generalization("or", [])
+    for f1 in clause1.list:
+        if f1 != formula:
+            new_clause.list.append(f1)
+
+    formula_compl = formula.complement()
+    for f2 in clause2.list:
+        if f2 != formula_compl:
+            new_clause.list.append(f2)
     return new_clause
 
 

From 9309f328598899a22473073dc65ac6d1354c88de Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Sun, 15 Sep 2013 15:42:05 +0200
Subject: [PATCH 18/19] Improve __eq__ of Formula

---
 pylogic/propositional/propositional_logic.py | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/pylogic/propositional/propositional_logic.py b/pylogic/propositional/propositional_logic.py
index 0782110..cb258dd 100644
--- a/pylogic/propositional/propositional_logic.py
+++ b/pylogic/propositional/propositional_logic.py
@@ -36,6 +36,7 @@ def __init__(self, *args):
             connective = None
             subformula1 = letter
             subformula2 = None
+            depth = 0
         elif len(args) == 2:
             if args[0] != "not" and args[0] != logic.CONN["not"]:
                 raise Exception("Wrong connective: " + args[0])
@@ -44,6 +45,7 @@ def __init__(self, *args):
             connective = "not"
             subformula1 = args[1]
             subformula2 = None
+            depth = subformula1.depth + 1
         else:
             if args[0] in list(set(logic.CONN.values()) - set("!")):
                 connective = [ item[0]
@@ -61,10 +63,13 @@ def __init__(self, *args):
                 raise Exception("Wrong formula: " + args[2])
             subformula1 = args[1]
             subformula2 = args[2]
+            depth = max(subformula1.depth, subformula2.depth)
+            depth = depth + 1
 
         self.connective = connective
         self.subformula1 = subformula1
         self.subformula2 = subformula2
+        self.depth = depth
 
 
     def __str__(self):
@@ -83,6 +88,8 @@ def __eq__(self, other):
             return False
         if self.connective == None and other.connective == None:
             return self.subformula1 == other.subformula1
+        if self.depth != other.depth:
+            return False
         else:
             return self.connective == other.connective \
                 and self.subformula1 == other.subformula1 \

From ac5cc45139618268946b0556678e5fb3d6978428 Mon Sep 17 00:00:00 2001
From: Paolo Sberna <reliablebeaver86-cs@yahoo.it>
Date: Fri, 20 Sep 2013 17:56:25 +0200
Subject: [PATCH 19/19] Add subsumption rule in the preliminary steps

Now resolution_rule takes almost 1/3 of the time less
---
 pylogic/propositional/propositional_logic.py  | 16 +++++++++++++++
 pylogic/propositional/resolution.py           | 20 +++++++++++++++++++
 .../test_propositional_propositional_logic.py | 13 ++++++++++++
 .../tests/test_propositional_resolution.py    | 12 +++++++++++
 4 files changed, 61 insertions(+)

diff --git a/pylogic/propositional/propositional_logic.py b/pylogic/propositional/propositional_logic.py
index cb258dd..cf5d224 100644
--- a/pylogic/propositional/propositional_logic.py
+++ b/pylogic/propositional/propositional_logic.py
@@ -304,6 +304,22 @@ def equivalent(self, other):
         return not other_list
 
 
+    def subsume(self, other):
+        """Check if the current generalization subsumes the 'other'
+        generalization"""
+        if self.connective != other.connective:
+            return False
+        if len(self.list) > len(other.list):
+            return False
+        other_list = list(other.list)
+        try:
+            for formula in self.list:
+                other_list.remove(formula)
+        except ValueError:
+            return False
+        return True
+
+
     def has_non_literal(self):
         """Check if in the list of formulas there are non-literal formulas."""
         if len(self.list) == 0:
diff --git a/pylogic/propositional/resolution.py b/pylogic/propositional/resolution.py
index e9bf362..3038b61 100644
--- a/pylogic/propositional/resolution.py
+++ b/pylogic/propositional/resolution.py
@@ -9,6 +9,7 @@ def preliminary_steps(clauses):
     manage_bottoms(clauses)
     manage_copies(clauses)
     manage_duplicated_clauses(clauses)
+    manage_subsumption_rule(clauses)
 
 def manage_tops(clauses):
     """Remove the clauses containg the top."""
@@ -75,6 +76,25 @@ def manage_duplicated_clauses(clauses):
     for i in reversed(removable):
         clauses.pop(i)
 
+def manage_subsumption_rule(clauses):
+    """Remove the clauses subsumed by another clause"""
+    i = 0
+    while i < len(clauses) - 1:
+        cl1 = clauses[i]
+        j = i + 1
+        deleted = False
+        while j < len(clauses) and not deleted:
+            cl2 = clauses[j]
+            if cl1.subsume(cl2):
+                del clauses[j]
+            elif cl2.subsume(cl1):
+                del clauses[i]
+                deleted = True
+            else:
+                j = j + 1
+        if not deleted:
+            i = i + 1
+
 
 def is_closed(expansion):
     """Given a list of clauses, return True if it contains an empty clause,
diff --git a/pylogic/tests/test_propositional_propositional_logic.py b/pylogic/tests/test_propositional_propositional_logic.py
index dde49da..24ac505 100644
--- a/pylogic/tests/test_propositional_propositional_logic.py
+++ b/pylogic/tests/test_propositional_propositional_logic.py
@@ -277,6 +277,10 @@ def test_cnf_particular(self):
 
 class TestGeneralization(unittest.TestCase):
     def setUp(self):
+        self.a1 = Formula("X")
+        self.a2 = Formula("Y")
+        self.a3 = Formula("Z")
+        self.a4 = Formula("W")
         self.f1 = Formula("&", Formula("X"), Formula("Y"))
         self.f2 = Formula("|", Formula("X"), Formula("Y"))
 
@@ -355,6 +359,15 @@ def test_equivalent(self):
         self.assertFalse(g1.equivalent(g4))
 
 
+    def test_subsume(self):
+        g1 = Generalization("or", [self.a1, self.a2])
+        g2 = Generalization("or", [self.a2, self.a1, self.a3])
+        g3 = Generalization("or", [self.a2, self.a1, self.a3, self.a4])
+        self.assertTrue(g1.subsume(g2))
+        self.assertTrue(g1.subsume(g3))
+        self.assertFalse(g3.subsume(g1))
+
+
     def test_has_non_literal(self):
         g1 = Generalization("and", [self.f1, Formula("Z"), self.f2])
         g2 = Generalization("or", [Formula("Z"), Formula("!", Formula("Y"))])
diff --git a/pylogic/tests/test_propositional_resolution.py b/pylogic/tests/test_propositional_resolution.py
index 5245a0a..18cb81f 100644
--- a/pylogic/tests/test_propositional_resolution.py
+++ b/pylogic/tests/test_propositional_resolution.py
@@ -104,6 +104,18 @@ def test_manage_duplicated_clauses(self):
         self.assertEqual(exp_clauses, clauses)
 
 
+    def test_manage_subsumption_rule(self):
+        clauses = [Generalization("or", [self.a1, self.a2]),
+                   Generalization("or", [self.a2, self.l1, self.a1]),
+                   Generalization("or", [self.a2, self.a1, self.a3]),
+                   Generalization("or", [self.a2, self.a3, self.a4]),
+                   Generalization("or", [self.a2, self.a3])]
+        exp_clauses = [Generalization("or", [self.a1, self.a2]),
+                       Generalization("or", [self.a2, self.a3])]
+        resolution.manage_subsumption_rule(clauses)
+        self.assertEqual(exp_clauses, clauses)
+
+
     def test_is_closed(self):
         expansion1 = [Generalization("or", [self.a1, self.l1]),
                       Generalization("or", [self.a2])]