Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

working resolution

  • Loading branch information...
commit aa191272620a13332a6740a86ac8f465f01433fc 1 parent 5162f32
@slomo authored
Showing with 53 additions and 10 deletions.
  1. +4 −2 main.py
  2. +31 −8 resolution.py
  3. +18 −0 resolution_test.py
View
6 main.py
@@ -2,7 +2,8 @@
import parser as tptp
import argparse as a
import operations as o
-#import resolution as r
+import resolution as r
+import fofTypes as f
def from_file(file):
return tptp.parse_file(file)
@@ -21,10 +22,11 @@ def from_string(string):
print(x)
else :
#x = from_string("(( not a and b) or q )")
- x = from_string("fof(ax, axiom, ~(( ~ a & b) | q ) ).")
+ x = from_string("fof(ax, axiom, ( ~ a | a ) & ( b | ~b ) ).")
tree = x[0][3]
print(tree)
+ tree = f.UnaryOperand("~",tree)
tree = o.transform(tree)
print("and transformed ...")
print(tree)
View
39 resolution.py
@@ -27,8 +27,10 @@ def proof(formula):
noDupes = []
[noDupes.append(i) for i in clauses if not noDupes.count(i)]
- return noDupes
+ print("splitted formulas", noDupes)
+
+ return resolute(noDupes)
# returns: <[]>
def split_any(disjunction):
@@ -48,7 +50,8 @@ def split_any(disjunction):
if type(formula) == f.BinaryOperand and formula.op == "&":
d = deepcopy(disjunction)
d.remove(formula)
- d1 = deepcopy(d).append(formula.terms[0])
+ d1 = deepcopy(d)
+ d1.append(formula.terms[0])
result_set.append(d1)
d.append(formula.terms[1])
@@ -67,23 +70,43 @@ def split_any(disjunction):
return result_set
+def is_tautology(d):
+
+ for q in d:
+ negate = f.UnaryOperand("~",q)
+ if negate in d:
+ return True
+ return False
+
+
+
def resolute(knf):
for disj in knf:
for elem in disj:
- if type(elem) is UnaryOperand:
+ # check weather i look for ~Z or Z
+ if type(elem) is f.UnaryOperand:
target = elem.term
else:
- target = UnaryOperand("~",elem)
+ target = f.UnaryOperand("~",elem)
- for other in deepcopy(knf):
+ for other_disj in deepcopy(knf):
+ if target in other_disj:
- if target in other:
- d = deepcopy(other)
+ d = deepcopy(other_disj)
d.remove(target)
d.extend(disj)
d.remove(elem)
- knf.append(d)
+ noDupes = []
+ [noDupes.append(i) for i in d if not noDupes.count(i)]
+ d = noDupes
+ if len(d) == 0:
+ return True
+ if not (d in knf) and not is_tautology(d):
+ print("Resoluting",disj,"with",other_disj,"to",d)
+ knf.append(d)
+
+ return False
View
18 resolution_test.py
@@ -0,0 +1,18 @@
+import resolution as r
+import unittest
+from fofTypes import *
+
+class ResolutionTest(unittest.TestCase):
+
+
+ def test_a_or_not_a(self):
+
+ formula = BinaryOperand("&",Identifier("a"),UnaryOperand("~",Identifier("a")))
+
+ self.assertTrue(r.proof(formula))
+
+
+
+if __name__ == '__main__':
+ unittest.main()
+
Please sign in to comment.
Something went wrong with that request. Please try again.