minor code cleanup

forseti/converter.py

@@ -7,9 +7,10 @@
 import forseti.parser as parser
 
 
-def convert_to_cnf(statement):
+def convert_formula(statement):
     """
-    Convert a given statement to Conjective Normal Form (CNF)
+    Converts a given formula into something we can use
+    as CNF clauses for resolution
 
     :param statement:
     :return: a CNF statement
@@ -36,6 +37,7 @@ def convert_to_cnf(statement):
 
 def _convert_iff(statement):
     """
+    Convert biconditionals into two conditionals joined by an And
 
     :param statement:
     :return:
@@ -55,6 +57,7 @@ def _convert_iff(statement):
 
 def _convert_if(statement):
     """
+    Convert conditional (A -> B) into (~A or B)
 
     :param statement:
     :return:
@@ -74,6 +77,7 @@ def _convert_if(statement):
 
 def _distribute_not(statement):
     """
+    Distribute not over and/or clauses (flipping them)
 
     :param statement:
     :return:
@@ -106,6 +110,8 @@ def _distribute_not(statement):
 
 def _distribute_or(statement):
     """
+    Distribute or over any nested and statements (so and becomes
+    outer most logical operator)
 
     :param statement:
     :return:
@@ -131,6 +137,7 @@ def _distribute_or(statement):
 
 def _is_cnf(statement, has_or=False):
     """
+    Is the given formula a CNF yet?
 
     :param statement:
     :param has_or:
@@ -153,6 +160,12 @@ def _is_cnf(statement, has_or=False):
 
 
 def _convert_pnf(statement):
+    """
+    Covert a formula into PNF form. Needs to be run after _convert_if!
+
+    :param statement:
+    :return:
+    """
     if isinstance(statement, str) or isinstance(statement, Symbol) or isinstance(statement, Herbrand) or isinstance(statement, Skolem):
         return statement
     if isinstance(statement, LogicalOperator):
@@ -190,6 +203,13 @@ def _convert_pnf(statement):
 
 
 def _is_pnf(statement, has_operator=False):
+    """
+    Is the given statement a PNF yet?
+
+    :param statement:
+    :param has_operator:
+    :return:
+    """
     if isinstance(statement, Symbol) or isinstance(statement, Herbrand) \
             or isinstance(statement, Skolem):
         return True
@@ -209,8 +229,13 @@ def _skolemization(statement, exists=None):
     """
     Remove existential quantifiers through skolemization
 
+    If the existential is inside
+
     :param statement:
-    :param exists:
+    :param exists: dictionary containing what skole to replace a variable with
+                    x -> Skole1
+                    y -> Skole2
+                    etc.
     :return:
     """
     if exists is None:
@@ -261,4 +286,4 @@ def _herbrandization(statement, forall=None):
     return statement
 
 if __name__ == "__main__":
-    print(convert_to_cnf(parser.parse("not(forall(x,if(A(x),C(x))))")))
+    print(convert_formula(parser.parse("not(forall(x,if(A(x),C(x))))")))

forseti/prover.py

@@ -52,7 +52,7 @@ def _add_statement(statement, add_to_list):
         :return:
         """
         statement = parser.parse(statement)
-        statement = converter.convert_to_cnf(statement)
+        statement = converter.convert_formula(statement)
         add_to_list.append(statement)
 
     def run_prover(self):

main.py

@@ -1,20 +1,20 @@
 from __future__ import print_function
 from forseti.prover import Prover
-import sys
 # pylint: disable=duplicate-code
 
-if __name__ == "__main__":
-    if len(sys.argv) == 1:
-        prover = Prover()
-        prover.add_formula("or(iff(G,H),iff(not(G),H))")
-        prover.add_goal("or(iff(not(G),not(H)),not(iff(G,H)))")
-        print(prover.run_prover())
-        print("\n".join(prover.get_proof()))
-    else:
-        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)))))")
-        print(prover.run_prover())
-        print("\n".join(prover.get_proof()))
+prover = Prover()
+prover.add_formula("or(iff(G,H),iff(not(G),H))")
+prover.add_goal("or(iff(not(G),not(H)),not(iff(G,H)))")
+print(prover.run_prover())
+print("\n".join(prover.get_proof()))
+
+
+print("\n\n")
+
+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)))))")
+print(prover.run_prover())
+print("\n".join(prover.get_proof()))

setup.py

@@ -14,7 +14,7 @@ def read(*paths):
 setup(
     # Metadata
     name='forseti',
-    version='0.6.6',
+    version='0.7.0',
     description='Formal Logic Framework',
     long_description=read('README.rst'),
     url='https://github.com/MasterOdin/forseti',

tests/converter_tester.py

@@ -7,50 +7,50 @@
 
 def test_cnf_converter_symbol():
     statement = Symbol("a")
-    statement = converter.convert_to_cnf(statement)
+    statement = converter.convert_formula(statement)
     expected = Symbol("a")
     assert_equal(expected, statement)
 
 
 def test_cnf_converter_equiv():
     statement = Iff(Symbol("a"), Symbol("b"))
-    statement = converter.convert_to_cnf(statement)
+    statement = converter.convert_formula(statement)
     expected = And(Or(Not(Symbol("a")), Symbol("b")),
                    Or(Not(Symbol("b")), Symbol("a")))
     assert_equal(expected, statement)
 
 
 def test_cnf_not_distribution():
     statement = Not(And(Symbol("a"), Symbol("b")))
-    statement = converter.convert_to_cnf(statement)
+    statement = converter.convert_formula(statement)
     expected = Or(Not(Symbol("a")), Not(Symbol("b")))
     assert_equal(expected, statement)
 
 
 def test_cnf_not_distribution_2():
     statement = Not(Or(And(Symbol("a"), Not(Symbol("b"))), Not(Symbol("c"))))
-    statement = converter.convert_to_cnf(statement)
+    statement = converter.convert_formula(statement)
     expected = And(Or(Not(Symbol("a")), Symbol("b")), Symbol("c"))
     assert_equal(expected, statement)
 
 
 def test_cnf_or_distribution():
     statement = Or(And(Symbol("a"), Symbol("b")), Symbol("c"))
-    statement = converter.convert_to_cnf(statement)
+    statement = converter.convert_formula(statement)
     expected = And(Or(Symbol("a"), Symbol("c")), Or(Symbol("b"), Symbol("c")))
     assert_equal(expected, statement)
 
 
 def test_cnf_negation():
     statement = Not(Not(And(Symbol("a"), Symbol("b"))))
-    statement = converter.convert_to_cnf(statement)
+    statement = converter.convert_formula(statement)
     expected = And(Symbol("a"), Symbol("b"))
     assert_equal(expected, statement)
 
 
 def test_convert_to_cnf():
     statement = Not(Iff(Symbol("a"), Symbol("c")))
-    statement = converter.convert_to_cnf(statement)
+    statement = converter.convert_formula(statement)
     a_symbol = Symbol("a")
     c_symbol = Symbol("c")
     expected = And(And(Or(c_symbol, a_symbol), Or(Not(a_symbol), a_symbol)),
@@ -61,11 +61,11 @@ def test_convert_to_cnf():
 
 def test_convert_to_cnf_2():
     statement = parser.parse("forall(x,if(A(x),and(B(x),C(x))))")
-    statement = converter.convert_to_cnf(statement)
+    statement = converter.convert_formula(statement)
     expected = "((B(Herbrand1) | ~A(Herbrand1)) & (C(Herbrand1) | ~A(Herbrand1)))"
     assert_equal(expected, str(statement))
 
 
 @raises(TypeError)
 def test_cnf_error_on_string():
-    converter.convert_to_cnf("invalid")
+    converter.convert_formula("invalid")

tests/prover_fol_tester.py

@@ -262,15 +262,6 @@ def test_fol_logic_2_9():
     assert_false(prover.run_prover())
 
 
-@SkipTest
-@with_setup(setup)
-def test_fol_logic_2_10():
-    prover = Prover()
-    prover.add_formula("exists(x,forall(y,A(x,y)))")
-    prover.add_goal("exists(x,A(x,a))")
-    assert_true(prover.run_prover())
-
-
 @with_setup(setup)
 def test_fol_logic_2_11():
     prover = Prover()