.gitignore

@@ -1,2 +1 @@
 __pycache__
-*.prof

Makefile

@@ -1,5 +0,0 @@
-.PHONY: prof
-
-prof:
-	python -m cProfile -o sine_patre.prof sine_patre.py
-	snakeviz sine_patre.prof

doc/grammar.bnf

@@ -5,7 +5,7 @@ IMP ::= OR imp OR
 OR ::= AND (or AND)*
 AND ::= NOT (and NOT)*
 NOT ::= not? GROUP
-GROUP ::= PRED | opar F cpar
+GROUP ::= NOT | opar F cpar
 PRED ::= pred opar TERM (comma TERM)* cpar
 
 TERM ::=

fol/__init__.py

@@ -1,13 +1,5 @@
 from fol import lexer
 from fol import parser
-from fol import kb
-from fol import pretty
-from fol import cnf
-from fol.unify import unify
-
-
-def p(text):
-    return parse(text)
 
 
 def parse(text):
@@ -16,11 +8,3 @@ def parse(text):
     p = parser.Parser(lex)
     root = p.parse()
     return root
-
-
-def term(text):
-    lex = lexer.Lexer()
-    lex.scan(text)
-    p = parser.Parser(lex)
-    root = p.parse_term()
-    return root

fol/cnf.py

@@ -1,233 +0,0 @@
-import fol
-
-
-class Counter:
-    def __init__(self):
-        self.values = {}
-        self.counter = 0
-
-    def get(self, name):
-        if name in self.values.keys():
-            return self.values[name]
-        self.values[name] = self.counter
-        self.counter += 1
-        return self.counter - 1
-
-    def begin(self):
-        self.values = {}
-
-
-def elim_imp(f):
-    res = fol.node.Node(f.name, f.value)
-
-    if f.name == 'IMP':
-        a = fol.node.Node('NOT')
-        a.add_child(elim_imp(f.children[0]))
-        res = fol.node.Node('OR')
-        res.add_child(elim_imp(a))
-        res.add_child(elim_imp(f.children[1]))
-        return res
-    else:
-        for c in f.children:
-            res.add_child(elim_imp(c))
-
-        return res
-
-
-def neg(f):
-    res = f.copy()
-
-    if f.name == 'NOT' and f.children[0].name in ['OR', 'AND']:
-        p = fol.node.Node('NOT')
-        p.add_child(neg(f.children[0].children[0]))
-        q = fol.node.Node('NOT')
-        q.add_child(neg(f.children[0].children[1]))
-
-        if f.children[0].name == 'OR':
-            res = fol.node.Node('AND')
-            res.add_child(neg(p))
-            res.add_child(neg(q))
-            return res
-        else:
-            res = fol.node.Node('OR')
-            res.add_child(neg(p))
-            res.add_child(neg(q))
-            return res
-
-    res = fol.node.Node(f.name, f.value)
-
-    for c in f.children:
-        res.add_child(neg(c))
-
-    return res
-
-
-def normalize(f, counter):
-    res = fol.node.Node(f.name, f.value)
-
-    if f.name == 'VAR':
-        res.value = f'x{counter.get(f.value)}'
-        return res
-
-    for child in f.children:
-        res.add_child(normalize(child, counter))
-
-    return res
-
-
-def prenex(f):
-    def mkneg(n):
-        res = fol.node.Node('NOT')
-        res.add_child(n)
-        return res
-
-    def inv(n):
-        if n.name == 'FORALL':
-            res = n.copy()
-            res.name = 'EXISTS'
-            return res
-        elif n.name == 'EXISTS':
-            res = n.copy()
-            res.name = 'FORALL'
-            return res
-        else:
-            return n.copy()
-
-    res = fol.node.Node(f.name, f.value)
-
-    if f.name == 'NOT':
-        arg = f.children[0]
-
-        if arg.name in ['FORALL', 'EXISTS']:
-            res = inv(arg)
-            res.children[1] = mkneg(arg.children[1])
-            return res
-
-    elif f.name in ['AND', 'OR', 'IMP']:
-        def apply_prenex(lhs, rhs, op_name):
-            swapped = False
-
-            if rhs.name in ['FORALL', 'EXISTS']:
-                lhs, rhs = rhs, lhs
-                swapped = True
-
-            if lhs.name in ['FORALL', 'EXISTS']:
-                left = lhs.children[1]
-                right = rhs
-                if swapped:
-                    left, right = right, left
-                var = lhs.children[0]
-
-                op = fol.node.Node(op_name)
-                op.add_child(left)
-                op.add_child(right)
-
-                res = fol.node.Node(lhs.name)
-                if op_name == 'IMP' and not swapped:
-                    res.name = 'EXISTS' if lhs.name == 'FORALL' else 'FORALL'
-                res.add_child(var)
-                res.add_child(op)
-                return res
-            return f.copy()
-
-        lhs = prenex(f.children[0])
-        rhs = prenex(f.children[1])
-
-        return apply_prenex(lhs, rhs, f.name)
-    return f.copy()
-
-
-def skolem(f):
-    def collect_exists(n):
-        res = []
-        if n.name == 'EXISTS':
-            res.append(n)
-        for child in n.children:
-            res.extend(collect_exists(child))
-        return res
-
-    def context(n, exists_quant, ctx=[]):
-        if n.equals(exists_quant):
-            return ctx
-
-        if n.name == 'FORALL':
-            ctx.append(n.children[0].value)
-
-        for child in n.children:
-            context(child, target, ctx)
-
-        return ctx
-
-    res = f.copy()
-    targets = collect_exists(res)
-
-    for target in targets:
-        idx = targets.index(target)
-        var_name = target.children[0].value
-
-        subst = {
-            var_name: fol.term(f'S{idx}')
-        }
-
-        ctx = context(f, target)
-
-        if len(ctx) > 0:
-            args = ','.join(ctx)
-            subst = {
-                var_name: fol.term(f's{idx}({args})')
-            }
-
-        res = res.subst(subst)
-
-    return res.remove_quant('EXISTS')
-
-
-def distrib(f):
-    if len(f.children) != 2:
-        return f
-
-    lhs = f.children[0]
-    rhs = f.children[1]
-
-    if f.name == 'OR' and rhs.name == 'AND':
-        a = distrib(lhs)
-        b = distrib(rhs.children[0])
-        c = distrib(rhs.children[1])
-        res = fol.node.Node('AND')
-        left = fol.node.Node('OR')
-        left.add_child(a)
-        left.add_child(b)
-        right = fol.node.Node('OR')
-        right.add_child(a)
-        right.add_child(c)
-        res.add_child(distrib(left))
-        res.add_child(distrib(right))
-        return res
-
-    if f.name == 'OR' and lhs.name == 'AND':
-        a = distrib(rhs)
-        b = distrib(lhs.children[0])
-        c = distrib(lhs.children[1])
-        res = fol.node.Node('AND')
-        left = fol.node.Node('OR')
-        left.add_child(b)
-        left.add_child(a)
-        right = fol.node.Node('OR')
-        right.add_child(c)
-        right.add_child(a)
-        res.add_child(distrib(left))
-        res.add_child(distrib(right))
-        return res
-
-    return f
-
-
-def cnf(f, counter=None):
-    if counter is None:
-        counter = Counter()
-
-    g = distrib(
-        skolem(prenex(normalize(neg(elim_imp(f)), counter)))
-    ).remove_quant('FORALL')
-
-    return g

fol/kb.py

@@ -1,168 +0,0 @@
-import fol
-
-
-class Kb:
-    def __init__(self):
-        self.base = []
-        self.counter = fol.cnf.Counter()
-
-    def make_f(self, h):
-        self.counter.begin()
-        f = h
-        if type(f) is str:
-            f = fol.p(f)
-        self.counter.begin()
-        f = fol.cnf.cnf(f, self.counter)
-
-        if f.name == 'OR':
-            f = f.list_of('OR')
-        else:
-            f = [f]
-
-        return f
-
-    def make_req(self, h):
-        f = h
-        if type(f) is str:
-            f = fol.p(f)
-
-        if f.name == 'OR':
-            f = f.list_of('OR')
-        else:
-            f = [f]
-
-        return f
-
-    def check_request(self, request):
-        for r in request:
-            if r.name not in ['NOT', 'PRED']:
-                raise Exception(f'invalid statement {repr(r)}')
-
-    def conds(self, statement):
-        result = []
-        for f in statement:
-            if f.name == 'NOT':
-                result.append(f.children[0])
-        return result
-
-    def conclusion(self, statement):
-        for f in statement:
-            if f.name != 'NOT':
-                return f
-        return None
-
-    @property
-    def rules(self):
-        res = []
-        for r in self.base:
-            if len(r) > 1:
-                res.append(r)
-        return res
-
-    @property
-    def facts(self):
-        res = []
-        for r in self.base:
-            if len(r) == 1:
-                res.append(r[0])
-        return res
-
-    def exists(self, f):
-        h = self.make_f(f)
-        for g in self.base:
-            if self.clause_equals(h, g):
-                return True
-        return False
-
-    def clause_equals(self, left, right):
-        if len(left) != len(right):
-            return False
-
-        for element in left:
-            if not self.clause_in(element, right):
-                return False
-
-        for element in right:
-            if not self.clause_in(element, left):
-                return False
-
-        return True
-
-    def clause_in(self, clause, lst):
-        for other in lst:
-            same = fol.unify(clause, other) is not None
-            if same:
-                return True
-        return False
-
-    def tell(self, request):
-        req = self.make_f(request)
-        self.check_request(req)
-        self.base.append(req)
-
-    def ask(self, request):
-        for i in range(20):
-            n = len(self.base)
-            self.update()
-            if n == len(self.base):
-                break
-
-        req = self.make_req(request)
-        results = []
-
-        for f in self.base:
-            s = fol.unify(f, req)
-            if s is not None:
-                results.append(s)
-
-        return results
-
-    def update(self):
-        for rule in self.rules:
-            conclusion = self.conclusion(rule)
-            solution = []
-            solutions = []
-            self.solve(rule, self.conds(rule), self.facts, solution, solutions)
-            for sol in solutions:
-                concl = conclusion.subst(sol)
-                if not self.exists(concl):
-                    self.base.append([concl])
-                    return
-
-    def merge_substs(self, substs):
-        res = {}
-        for s in substs:
-            for k in s.keys():
-                if k in res.keys() and not res[k].equals(s[k]):
-                    return None
-                res[k] = s[k]
-        return res
-
-    def solve(self, rule, conds, facts, solution, solutions):
-        if len(conds) == 0:
-            substs = []
-
-            for sol in solution:
-                s = fol.unify(sol[0], sol[1])
-                if s is not None:
-                    substs.append(s)
-
-            s = self.merge_substs(substs)
-
-            if s is not None:
-                solutions.append(s)
-            return
-
-        for cond in conds:
-            for fact in facts:
-                solution.append((cond, fact))
-
-                self.solve(
-                    rule,
-                    [c for c in conds if c != cond],
-                    [f for f in facts if f != fact],
-                    solution,
-                    solutions
-                )
-
-                solution.pop()

fol/lexer.py

@@ -66,10 +66,7 @@ class Lexer:
         cursor = self.cursor
         value = ''
 
-        while cursor < len(self.text) and (
+        while cursor < len(self.text) and self.text[cursor].islower():
-                self.text[cursor].islower()
-                or self.text[cursor].isdigit()
-        ):
             value += self.text[cursor]
             cursor += 1
 
@@ -83,10 +80,7 @@ class Lexer:
         cursor = self.cursor
         value = ''
 
-        while cursor < len(self.text) and (
+        while cursor < len(self.text) and self.text[cursor].isupper():
-                self.text[cursor].isupper()
-                or self.text[cursor].isdigit()
-        ):
             value += self.text[cursor]
             cursor += 1
 

fol/node.py

@@ -1,102 +0,0 @@
-import fol
-
-
-class Node:
-    def __init__(self, name, value=None):
-        self.name = name
-        self.value = value
-        self.children = []
-
-    def add_child(self, child):
-        self.children.append(child)
-
-    def __repr__(self):
-        return fol.pretty.get(self)
-
-    def __str__(self):
-        res = self.name
-        if self.value is not None:
-            res += f'[{self.value}]'
-
-        if len(self.children) > 0:
-            res += '('
-            sep = ''
-
-            for child in self.children:
-                res += sep + str(child)
-                sep = ','
-            res += ')'
-        return res
-
-    def copy(self):
-        node = Node(self.name, self.value)
-        for child in self.children:
-            node.add_child(child.copy())
-        return node
-
-    def remove_quant(self, name):
-        if self.name == name:
-            itr = self
-            while itr.name == name:
-                itr = itr.children[1]
-            return itr
-
-        node = Node(self.name, self.value)
-        for child in self.children:
-            if child.name == name:
-                node.add_child(child.children[1].remove_quant(name))
-            else:
-                node.add_child(child.remove_quant(name))
-        return node
-
-    def subst(self, values):
-        node = Node(self.name, self.value)
-        if self.name == 'VAR' and self.value in values.keys():
-            node = values[self.value]
-        else:
-            for child in self.children:
-                node.add_child(child.subst(values))
-
-        return node
-
-    def equals(self, rhs):
-        if self.name != rhs.name or self.value != rhs.value:
-            return False
-
-        if len(self.children) != len(rhs.children):
-            return False
-
-        for i in range(len(self.children)):
-            if not self.children[i].equals(rhs.children[i]):
-                return False
-
-        return True
-
-    def list_of(self, name):
-        result = []
-
-        if self.name == name:
-            for c in self.children:
-                if c.name != name:
-                    result.append(c)
-                result.extend(c.list_of(name))
-
-        return result
-
-    def flatten(self):
-        result = self.list_of(self.name)
-        print(result)
-        root = fol.node.Node(self.name, self.value)
-        root.children = result
-        return root
-
-    def find_by_name(self, name):
-        if self.name == name:
-            return [self]
-
-        res = []
-
-        for c in self.children:
-            res.extend(c.find_by_name(name))
-
-        return res

fol/parser.py

@@ -1,4 +1,26 @@
-from fol.node import Node
+class Node:
+    def __init__(self, name, value=None):
+        self.name = name
+        self.value = value
+        self.children = []
+
+    def add_child(self, child):
+        self.children.append(child)
+
+    def __str__(self):
+        res = self.name
+        if self.value is not None:
+            res += f'[{self.value}]'
+
+        if len(self.children) > 0:
+            res += '('
+            sep = ''
+
+            for child in self.children:
+                res += sep + str(child)
+                sep = ','
+            res += ')'
+        return res
 
 
 class Parser:
@@ -92,7 +114,7 @@ class Parser:
     def parse_not(self):
         if self.consume('NOT'):
             node = Node('NOT')
-            node.add_child(self.parse_group())
+            node.add_child(self.parse_pred())
             return node
 
         return self.parse_group()

fol/pretty.py

@@ -1,23 +0,0 @@
-def get(f):
-    if f.name == 'EXISTS':
-        return f'\\exist {get(f.children[0])}({get(f.children[1])})'
-
-    if f.name == 'NOT':
-        return '~' + get(f.children[0])
-
-    if f.name == 'AND':
-        return '(' + " & ".join([get(c) for c in f.children]) + ')'
-
-    if f.name == 'OR':
-        return '(' + " | ".join([get(c) for c in f.children]) + ')'
-
-    if f.name in ['PRED', 'FUN']:
-        return f.value + "(" + ", ".join([get(c) for c in f.children]) + ")"
-
-    if f.name in ['VAR', 'CONST']:
-        return f.value
-
-    if f.name == 'IMP':
-        return '(' + get(f.children[0]) + ' -> ' + get(f.children[1]) + ')'
-
-    raise Exception(f'cannot print f = {f.name}')

fol/tests/test_cnf.py

@@ -1,128 +0,0 @@
-import pytest
-import fol
-
-
-@pytest.mark.parametrize(['imp', 'res'], [
-    ('\\exists x (Pre(y) -> Post(y))',
-     '\\exists x (~Pre(y) | Post(y))'),
-    ('Pre(x) -> Post(x)', '~Pre(x) | Post(x)'),
-    ('Pre(x) -> (Aux(y) -> Post(x))',
-     '~Pre(x) | (~Aux(y) | Post(x))'),
-    ('(Pre(x) & Aux(y)) -> Post(x)', '~(Pre(x) & Aux(y)) | Post(x)')
-])
-def test_cnf_imp(imp, res):
-    assert fol.cnf.elim_imp(fol.p(imp)).equals(fol.p(res))
-
-
-@pytest.mark.parametrize(['f', 'res'], [
-    ('~(Pre(x) | Post(y))', '~Pre(x) & ~Post(y)'),
-    ('~(Pre(x) & Post(y))', '~Pre(x) | ~Post(y)'),
-    ('~(Pre(x) & (Post(y) | Post(z)))',
-     '~Pre(x) | (~Post(y) & ~Post(z))'),
-])
-def test_cnf_neg(f, res):
-    assert fol.cnf.neg(fol.p(f)).equals(fol.p(res))
-
-
-@pytest.mark.parametrize(['f', 'res'], [
-    ('Pre(x) -> Post(x)', 'Pre(x0) -> Post(x0)'),
-    ('Pre(x) -> Post(y)', 'Pre(x0) -> Post(x1)'),
-    ('Pre(x, y) -> Post(y, x)', 'Pre(x0, x1) -> Post(x1, x0)'),
-    ('Pre(f(x)) -> Post(g(g(y), x))',
-     'Pre(f(x0)) -> Post(g(g(x1), x0))'),
-])
-def test_cnf_normalize(f, res):
-    counter = fol.cnf.Counter()
-    assert fol.cnf.normalize(fol.p(f), counter).equals(fol.p(res))
-
-
-@pytest.mark.parametrize(['f', 'res'], [
-    # FOR ALL
-    ('~(\\forall x Pre(x))', '\\exists x ~Pre(x)'),
-
-    ('(\\forall x Pre(x)) & Post(x)',
-     '\\forall x (Pre(x) & Post(x))'),
-
-    ('(\\forall x Pre(x)) | Post(x)',
-     '\\forall x (Pre(x) | Post(x))'),
-
-    ('(\\forall x Pre(x)) -> Post(x)',
-     '\\exists x (Pre(x) -> Post(x))'),
-
-    ('Pre(x) & (\\forall x Post(x))',
-     '\\forall x (Pre(x) & Post(x))'),
-
-    ('Pre(x) | (\\forall x Post(x))',
-     '\\forall x (Pre(x) | Post(x))'),
-
-    ('Pre(x) -> (\\forall x Post(x))',
-     '\\forall x (Pre(x) -> Post(x))'),
-    # EXISTS
-    ('~(\\exists x Pre(x))', '\\forall x ~Pre(x)'),
-
-    ('(\\exists x Pre(x)) & Post(x)',
-     '\\exists x (Pre(x) & Post(x))'),
-
-    ('(\\exists x Pre(x)) | Post(x)',
-     '\\exists x (Pre(x) | Post(x))'),
-
-    ('(\\exists x Pre(x)) -> Post(x)',
-     '\\forall x (Pre(x) -> Post(x))'),
-
-    ('Pre(x) & (\\exists x Post(x))',
-     '\\exists x (Pre(x) & Post(x))'),
-
-    ('Pre(x) | (\\exists x Post(x))',
-     '\\exists x (Pre(x) | Post(x))'),
-
-    ('Pre(x) -> (\\exists x Post(x))',
-     '\\exists x (Pre(x) -> Post(x))'),
-
-])
-def test_cnf_prenex(f, res):
-    assert fol.cnf.prenex(fol.p(f)).equals(fol.p(res))
-
-
-@pytest.mark.parametrize(['imp', 'res'], [
-    ('\\exists x (Pre(x) -> Post(x))', 'Pre(S0) -> Post(S0)'),
-
-    ('\\exists x (\\exists y (Pre(x) -> Post(y)))',
-     'Pre(S0) -> Post(S1)'),
-
-    ('\\forall a (\\exists x (Pre(a, x) -> Post(x)))',
-     '\\forall a (Pre(a, s0(a)) -> Post(s0(a)))'),
-
-    ('\\forall a (\\forall b (\\exists x (Pre(a, x) -> Post(x))))',
-     '\\forall a (\\forall b (Pre(a, s0(a, b)) -> Post(s0(a, b))))'),
-
-    ('\\forall a (\\exists x (\\forall b (Pre(x) -> Post(x))))',
-     '\\forall a (\\forall b (Pre(s0(a)) -> Post(s0(a))))'),
-
-    ('\\forall a (\\exists x (\\forall b (Pre(x) -> Post(x))))',
-     '\\forall a (\\forall b (Pre(s0(a)) -> Post(s0(a))))'),
-])
-def test_cnf_skolem(imp, res):
-    assert fol.cnf.skolem(fol.p(imp)).equals(fol.p(res))
-
-
-@pytest.mark.parametrize(['f', 'oracle'], [
-    ('Pre(x) | (Aux(x) & Post(x))',
-     '(Pre(x) | Aux(x)) & (Pre(x) | Post(x))'),
-    ('(Aux(x) & Post(x)) | Pre(x)',
-     '(Aux(x) | Pre(x)) & (Post(x) | Pre(x))')
-])
-def test_distrib(oracle, f):
-    assert fol.cnf.distrib(fol.p(f)).equals(fol.p(oracle))
-
-
-@pytest.mark.parametrize(['f', 'oracle'], [
-    ('Friend(x, y) -> Friend(y, x)',
-     '~Friend(x0, x1) | Friend(x1, x0)'),
-
-    ('(Friend(x, y) & Friend(y, z)) -> Friend(x, z)',
-     '(~Friend(x0, x1) | ~Friend(x1, x2)) | Friend(x0, x2)')
-])
-def test_cnf(oracle, f):
-    print(fol.pretty.get(fol.p(f)))
-    print(fol.pretty.get(fol.cnf.cnf(fol.p(f))))
-    assert fol.cnf.cnf(fol.p(f)).equals(fol.p(oracle))

fol/tests/test_kb.py

@@ -1,11 +0,0 @@
-import fol
-
-
-def test_kb_simple():
-    kb = fol.kb.Kb()
-    kb.tell('Friend(ALICE, BOB)')
-
-    res = kb.ask('Friend(ALICE, x)')
-
-    assert len(res) == 1
-    assert res[0]['x'].value == 'BOB'

fol/tests/test_subst.py

@@ -1,32 +0,0 @@
-import fol
-
-
-def test_empty_subst():
-    root = fol.parse('Happy(x)').subst({})
-    assert 'PRED[Happy](VAR[x])' == str(root)
-
-
-def test_one_var_subst():
-    root = fol.parse('Happy(x)').subst({'x': fol.term('z')})
-    assert 'PRED[Happy](VAR[z])' == str(root)
-
-
-def test_one_function_subst():
-    root = fol.parse('Happy(x)').subst({'x': fol.term('f(z)')})
-    assert 'PRED[Happy](FUN[f](VAR[z]))' == str(root)
-
-
-def test_ambiguous_subst():
-    root = fol.parse('Happy(x)').subst({
-        'x': fol.term('y'),
-        'y': fol.term('z'),
-    })
-    assert 'PRED[Happy](VAR[y])' == str(root)
-
-
-def test_ambiguous_reverse_subst():
-    root = fol.parse('Happy(x, y)').subst({
-        'y': fol.term('z'),
-        'x': fol.term('y'),
-    })
-    assert 'PRED[Happy](VAR[y],VAR[z])' == str(root)

fol/tests/test_unify.py

@@ -1,87 +0,0 @@
-import fol
-
-
-def test_unify_simple():
-    subst = fol.unify(
-        fol.p('Hello(x)'),
-        fol.p('Hello(ALICE)')
-    )
-
-    assert subst is not None
-    assert len(subst) == 1
-    assert str(subst['x']) == 'CONST[ALICE]'
-
-
-def test_unify_equals():
-    subst = fol.unify(
-        fol.p('Hello(ALICE)'),
-        fol.p('Hello(ALICE)')
-    )
-
-    assert subst is not None
-    assert len(subst) == 0
-
-
-def test_unify_different_predicate_name():
-    subst = fol.unify(
-        fol.p('Hello(x)'),
-        fol.p('World(ALICE)')
-    )
-
-    assert subst is None
-
-
-def test_unify_fun():
-    subst = fol.unify(
-        fol.p('Hello(x, f(x))'),
-        fol.p('Hello(ALICE, f(ALICE))')
-    )
-
-    assert subst is not None
-    assert len(subst) == 1
-    assert str(subst['x']) == 'CONST[ALICE]'
-
-
-def test_unify_two_vars():
-    subst = fol.unify(
-        fol.p('Hello(z, f(x), z)'),
-        fol.p('Hello(ALICE, f(BOB), ALICE)')
-    )
-
-    assert subst is not None
-    assert len(subst) == 2
-    assert str(subst['x']) == 'CONST[BOB]'
-    assert str(subst['z']) == 'CONST[ALICE]'
-
-
-def test_unify_fun_var():
-    subst = fol.unify(
-        fol.p('Hello(z, f(x), z)'),
-        fol.p('Hello(ALICE, a, ALICE)')
-    )
-
-    assert subst is not None
-    assert len(subst) == 2
-    assert str(subst['a']) == 'FUN[f](VAR[x])'
-    assert str(subst['z']) == 'CONST[ALICE]'
-
-
-def test_unify_formula():
-    subst = fol.unify(
-        fol.p('Friend(x, y) -> Friend(y, x)'),
-        fol.p('Friend(ALICE, y) -> Friend(BOB, x)')
-    )
-
-    assert subst is not None
-    assert len(subst) == 2
-    assert str(subst['x']) == 'CONST[ALICE]'
-    assert str(subst['y']) == 'CONST[BOB]'
-
-
-def test_unify_formula_contradiction():
-    subst = fol.unify(
-        fol.p('Friend(x, y) -> Friend(y, x)'),
-        fol.p('Friend(ALICE, y) -> Friend(BOB, CLARA)')
-    )
-
-    assert subst is None

fol/unify.py

@@ -1,84 +0,0 @@
-import fol
-
-
-def unify(lhs, rhs):
-    s = {}
-    return _unify(lhs, rhs, s)
-
-
-def _unify(lhs, rhs, s):
-    if s is None:
-        return None
-    elif is_equal(lhs, rhs):
-        return s
-    elif is_var(lhs):
-        return unify_var(lhs, rhs, s)
-    elif is_var(rhs):
-        return unify_var(rhs, lhs, s)
-    elif is_compound(lhs) and is_compound(rhs) and (
-            lhs.name == rhs.name and lhs.value == rhs.value
-            ):
-
-        return _unify(
-            lhs.children,
-            rhs.children,
-            s
-        )
-    elif is_list(lhs) and is_list(rhs):
-        if len(lhs) != len(rhs):
-            return None
-        elif len(lhs) == 0:
-            return s
-        elif len(lhs) == 1:
-            return _unify(lhs[0], rhs[0], s)
-        else:
-            return _unify(lhs[1:], rhs[1:], _unify(lhs[0], rhs[0], s))
-    else:
-        return None
-
-
-def unify_var(var, x, s):
-    if var.value in s.keys():
-        return _unify(s[var.value], x, s)
-    elif x in s.keys():
-        return _unify(var, s[x], s)
-    elif occur_check(var, x):
-        return None
-    else:
-        s[var.value] = x
-        return s
-
-
-def occur_check(var, x):
-    if var.name == x.name and var.value == x.value:
-        return True
-
-    for child in x.children:
-        if occur_check(var, child):
-            return True
-
-    return False
-
-
-def is_compound(f):
-    if type(f) is fol.node.Node:
-        return len(f.children) > 0
-    return False
-
-
-def is_equal(lhs, rhs):
-    if type(lhs) is str and type(rhs) is str:
-        return lhs == rhs
-
-    if type(lhs) is fol.node.Node and type(rhs) is fol.node.Node:
-        return lhs.equals(rhs)
-
-    return False
-
-
-def is_var(f):
-    return type(f) is fol.node.Node and f.name == 'VAR'
-
-
-def is_list(value):
-    return type(value) is list

sine_patre.py

@@ -1,13 +1,2 @@
-import fol
-
 if __name__ == '__main__':
-    kb = fol.kb.Kb()
+    print('Sine Patre')
-    try:
-        kb.tell('Friend(ALICE, BOB)')
-        kb.tell('Friend(BOB, CLAIRE)')
-        kb.tell('Friend(x, y) -> Friend(y, x)')
-        kb.tell('(Friend(x, y) & Friend(y, z)) -> Friend(x, z)')
-
-        print(kb.ask('Friend(ALICE, x)'))
-    except KeyboardInterrupt:
-        pass