✨ forward chaining v0.

.gitignore

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

Makefile

@@ -0,0 +1,5 @@
+.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 ::= NOT | opar F cpar
+GROUP ::= PRED | opar F cpar
 PRED ::= pred opar TERM (comma TERM)* cpar
 
 TERM ::=

fol/__init__.py

@@ -1,5 +1,13 @@
 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):
@@ -8,3 +16,11 @@ 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

@@ -0,0 +1,233 @@
+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

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

fol/node.py

@@ -0,0 +1,102 @@
+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,26 +1,4 @@
-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
+from fol.node import Node
 
 
 class Parser:
@@ -114,7 +92,7 @@ class Parser:
     def parse_not(self):
         if self.consume('NOT'):
             node = Node('NOT')
-            node.add_child(self.parse_pred())
+            node.add_child(self.parse_group())
             return node
 
         return self.parse_group()

fol/pretty.py

@@ -0,0 +1,23 @@
+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

@@ -0,0 +1,128 @@
+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

@@ -0,0 +1,11 @@
+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

@@ -0,0 +1,32 @@
+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

@@ -0,0 +1,87 @@
+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

@@ -0,0 +1,84 @@
+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,2 +1,13 @@
+import fol
+
 if __name__ == '__main__':
-    print('Sine Patre')
+    kb = fol.kb.Kb()
+    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