Write a bunch more test cases based on Bram handouts

forseti/exceptions.py

@@ -0,0 +1,2 @@
+class TimeoutException(Exception):
+    pass

forseti/prover.py

@@ -3,23 +3,28 @@
 """
 # pylint: disable=fixme
 from copy import deepcopy
+import time
+
 from forseti.formula import Formula, Not, And, Or, Skolem, Herbrand, Predicate
 from forseti import converter, parser
 import forseti.util as util
+from forseti import exceptions
 
 
 class Prover(object):
     """
     Prover class
     """
 
-    def __init__(self):
+    def __init__(self, timeout=30):
         self._cnf_list = []
         self.parents = []
         self.formulas = []
         self.goals = []
         self._goals = []
         self.proof_found = False
+        self.proof_time = 0
+        self.proof_timeout = timeout
 
     def add_formula(self, statement):
         """
@@ -80,7 +85,7 @@ def run_prover(self):
             self._cnf_list[i] = sorted(self._cnf_list[i])
         for i in range(len(self._cnf_list)):
             self.parents.append([])
-        self.proof_found = self._resolve()
+        self.proof_found, self.proof_time = self._resolve()
         return self.proof_found
 
     @staticmethod
@@ -133,9 +138,12 @@ def _resolve(self):
 
         :return:
         """
+        start_time = time.time()
         i = 0
         checked = list()
         while i < len(self._cnf_list):
+            if (time.time() - start_time) > self.proof_timeout:
+                raise exceptions.TimeoutException('Proof timeout reached')
             j = i + 1
             while j < len(self._cnf_list):
                 if [i, j] in checked:
@@ -165,7 +173,7 @@ def _resolve(self):
                         if len(new_cnf) == 0:
                             self._cnf_list.append([])
                             self.parents.append([i, j])
-                            return True
+                            return True, time.time() - start_time
                         if not util.is_tautology(new_cnf) and \
                            new_cnf not in self._cnf_list:
                             have_resolve = True
@@ -180,7 +188,7 @@ def _resolve(self):
                     break
                 j += 1
             i += 1
-        return False
+        return False, time.time() - start_time
 
     def _tautology_elimination(self):
         """
@@ -308,4 +316,4 @@ def get_proof(self):
     prover.add_formula("exists(x,forall(y,A(x,y)))")
     prover.add_goal("exists(x,A(x,a))")
     print(prover.run_prover())
-    print("\n".join(prover.get_proof()))
+    print("\n".join(prover.get_proof()))

setup.py

@@ -11,6 +11,7 @@ def read(*paths):
     with open(os.path.join(*paths), 'r') as open_file:
         return open_file.read()
 
+
 setup(
     # Metadata
     name='forseti',

tests/bram_testcases/README.md

@@ -13,4 +13,4 @@ The handouts, in order of difficulty in given arguments and for ATP testing:
 * [Propositional Logic Arguments](handouts/PropLogicArguments.pdf)
 * [Propositional Logic Arguments II](handouts/PropLogicArgumentsII.pdf)
 * [Predicate Logic Arguments](handouts/PredicateLogicArguments.pdf)
-* [First Order Logic Proofs](handouts/FOLProofs.pdf)
+* [First Order Logic Proofs](handouts/FOLProofsII.pdf)

tests/bram_testcases/test_fol_proofs_i.py

@@ -0,0 +1,149 @@
+import unittest
+from forseti.prover import Prover
+from forseti.formula import Predicate, Skolem, Herbrand
+
+
+class TestFOLProofsI(unittest.TestCase):
+    def setUp(self):
+        Predicate.reset()
+        Skolem.reset()
+        Herbrand.reset()
+
+    def test_problem_01(self):
+        prover = Prover()
+        prover.add_formula("forall(x,if(A(x),B(x)))")
+        prover.add_formula("forall(x,if(B(x),C(x)))")
+        prover.add_goal("forall(x,if(A(x),C(x)))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_02(self):
+        prover = Prover()
+        prover.add_formula("forall(x,if(A(x),and(B(x),C(x))))")
+        prover.add_formula("forall(x,if(A(x),not(C(x))))")
+        prover.add_goal("not(A(a))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_03(self):
+        prover = Prover()
+        prover.add_formula("forall(x,if(A(x),B(x)))")
+        prover.add_formula("forall(x,if(not(A(x)),C(x)))")
+        prover.add_goal("forall(x,if(not(B(x)),not(C(x))))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_04(self):
+        prover = Prover()
+        prover.add_formula("exists(x,and(A(x),not(B(x))))")
+        prover.add_formula("exists(x,and(A(x),not(C(x))))")
+        prover.add_formula("exists(x,and(not(B(x)),D(x)))")
+        prover.add_goal("exists(x,and(and(A(x),not(B(x))),D(x)))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_05(self):
+        prover = Prover()
+        prover.add_formula("forall(x,if(A(x),F(x)))")
+        prover.add_formula("if(exists(x,F(x)),not(exists(y,G(y))))")
+        prover.add_goal("forall(x,if(exists(y,A(y)),not(G(x))))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_06(self):
+        prover = Prover()
+        prover.add_formula("exists(x,or(A(x),not(B(x))))")
+        prover.add_formula("forall(x,if(and(A(x),not(B(x))),C(x)))")
+        prover.add_goal("exists(x,C(x))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_07(self):
+        prover = Prover()
+        prover.add_formula("forall(x,not(F(x,x)))")
+        prover.add_formula("if(not(forall(x,G(x))),exists(y,F(y,a)))")
+        prover.add_goal("exists(z,and(G(z),F(z,z)))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_08(self):
+        prover = Prover()
+        prover.add_formula("forall(x,exists(y,and(F(x),G(x,y))))")
+        prover.add_goal("exists(y,forall(x,and(F(x),G(x,y))))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_09(self):
+        prover = Prover()
+        prover.add_formula("exists(x,and(F(x),forall(y,if(G(y),L(x,y)))))")
+        prover.add_formula("forall(x,if(F(x),forall(y,if(M(y),not(L(x,y))))))")
+        prover.add_goal("forall(x,if(G(x),not(M(x))))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_10(self):
+        prover = Prover()
+        prover.add_formula("or(F(a),exists(y,G(y,a)))")
+        prover.add_formula("or(F(b),exists(y,not(G(y,a))))")
+        prover.add_goal("exists(y,G(y,a))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_11(self):
+        prover = Prover()
+        prover.add_formula("forall(x,not(J(x)))")
+        prover.add_formula("if(exists(y,or(H(b,y),R(y,y))),exists(x,J(x)))")
+        prover.add_goal("forall(y,not(or(H(b,y),R(y,y))))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_12(self):
+        prover = Prover()
+        prover.add_formula("forall(z,iff(L(z),H(z)))")
+        prover.add_formula("forall(x,not(or(H(x),not(B(x)))))")
+        prover.add_goal("not(L(b))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_13(self):
+        prover = Prover()
+        prover.add_formula("or(not(forall(x,K(x,x))),forall(y,H(y,y)))")
+        prover.add_goal("exists(z,if(not(H(z,z)),not(K(z,z))))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_14(self):
+        prover = Prover()
+        prover.add_formula("forall(x,forall(y,or(F(x),G(x,y))))")
+        prover.add_formula("exists(x,F(x))")
+        prover.add_goal("exists(x,exists(y,G(x,y)))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_15(self):
+        prover = Prover()
+        prover.add_formula("forall(x,forall(y,forall(z,if(and(L(x,y),L(y,z)),"
+                           "L(x,z)))))")
+        prover.add_formula("forall(x,forall(y,if(L(x,y),L(y,x))))")
+        prover.add_goal("forall(x,L(x,x))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_16(self):
+        prover = Prover()
+        prover.add_formula("forall(x,if(S(x),exists(y,and(S(y),forall(z,"
+                           "iff(B(z,y),and(B(z,x),B(z,z))))))))")
+        prover.add_formula("forall(x,not(B(x,x)))")
+        prover.add_formula("exists(x,S(x))")
+        prover.add_goal("exists(x,and(S(x),forall(y,not(B(y,x)))))")
+        self.assertTrue(prover.run_prover())
+
+    def test_problem_17(self):
+        prover = Prover()
+        prover.add_formula("forall(x,forall(y,if(and(A(x),B(y)),C(x,y))))")
+        prover.add_formula("exists(y,and(F(y),forall(z,if(H(z),C(y,z)))))")
+        prover.add_formula("forall(x,forall(y,forall(z,if(and(L(x,y),L(y,z)),"
+                           "L(x,z)))))")
+        prover.add_formula("forall(x,if(F(x),B(x)))")
+        prover.add_goal("forall(z,forall(y,if(and(A(z),H(y)),C(z,y))))")
+        self.assertFalse(prover.run_prover())
+
+    def test_problem_18(self):
+        self.skipTest('Should work')
+        prover = Prover()
+        prover.add_formula("forall(x,if(exists(y,and(A(y),B(x,y))),C(x)))")
+        prover.add_formula("exists(y,and(D(y),exists(x,and(F(x),and(G(x),B(y,x))))))")
+        prover.add_formula("forall(x,if(F(x),A(x)))")
+        prover.add_formula(
+            "if(exists(x,and(C(x),D(x))),if(exists(y,and(D(y),exists(z,B(y,z)))),forall(x,F(x))))")
+        prover.add_goal("forall(x,A(x))")
+        self.assertTrue(prover.run_prover())
+
+
+if __name__ == '__main__':
+    unittest.main()

tests/bram_testcases/test_fol_proofs_ii.py

@@ -0,0 +1,10 @@
+import unittest
+from forseti.prover import Prover
+
+
+class TestFOLProofsII(unittest.TestCase):
+    pass
+
+
+if __name__ == '__main__':
+    unittest.main()