Compare commits
No commits in common. "bfd64b20b6b7c27d5b4661fccc16202822c894db" and "badb08ec0525c8faa68fba017ce35f56b9ac71b5" have entirely different histories.
bfd64b20b6
...
badb08ec05
|
@ -1,2 +1 @@
|
||||||
__pycache__
|
__pycache__
|
||||||
*.prof
|
|
5
Makefile
5
Makefile
|
@ -1,5 +0,0 @@
|
||||||
.PHONY: prof
|
|
||||||
|
|
||||||
prof:
|
|
||||||
python -m cProfile -o sine_patre.prof sine_patre.py
|
|
||||||
snakeviz sine_patre.prof
|
|
|
@ -5,7 +5,7 @@ IMP ::= OR imp OR
|
||||||
OR ::= AND (or AND)*
|
OR ::= AND (or AND)*
|
||||||
AND ::= NOT (and NOT)*
|
AND ::= NOT (and NOT)*
|
||||||
NOT ::= not? GROUP
|
NOT ::= not? GROUP
|
||||||
GROUP ::= PRED | opar F cpar
|
GROUP ::= NOT | opar F cpar
|
||||||
PRED ::= pred opar TERM (comma TERM)* cpar
|
PRED ::= pred opar TERM (comma TERM)* cpar
|
||||||
|
|
||||||
TERM ::=
|
TERM ::=
|
||||||
|
|
|
@ -1,13 +1,5 @@
|
||||||
from fol import lexer
|
from fol import lexer
|
||||||
from fol import parser
|
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):
|
def parse(text):
|
||||||
|
@ -16,11 +8,3 @@ def parse(text):
|
||||||
p = parser.Parser(lex)
|
p = parser.Parser(lex)
|
||||||
root = p.parse()
|
root = p.parse()
|
||||||
return root
|
return root
|
||||||
|
|
||||||
|
|
||||||
def term(text):
|
|
||||||
lex = lexer.Lexer()
|
|
||||||
lex.scan(text)
|
|
||||||
p = parser.Parser(lex)
|
|
||||||
root = p.parse_term()
|
|
||||||
return root
|
|
||||||
|
|
233
fol/cnf.py
233
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
|
|
168
fol/kb.py
168
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()
|
|
10
fol/lexer.py
10
fol/lexer.py
|
@ -66,10 +66,7 @@ class Lexer:
|
||||||
cursor = self.cursor
|
cursor = self.cursor
|
||||||
value = ''
|
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]
|
value += self.text[cursor]
|
||||||
cursor += 1
|
cursor += 1
|
||||||
|
|
||||||
|
@ -83,10 +80,7 @@ class Lexer:
|
||||||
cursor = self.cursor
|
cursor = self.cursor
|
||||||
value = ''
|
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]
|
value += self.text[cursor]
|
||||||
cursor += 1
|
cursor += 1
|
||||||
|
|
||||||
|
|
102
fol/node.py
102
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
|
|
|
@ -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:
|
class Parser:
|
||||||
|
@ -92,7 +114,7 @@ class Parser:
|
||||||
def parse_not(self):
|
def parse_not(self):
|
||||||
if self.consume('NOT'):
|
if self.consume('NOT'):
|
||||||
node = Node('NOT')
|
node = Node('NOT')
|
||||||
node.add_child(self.parse_group())
|
node.add_child(self.parse_pred())
|
||||||
return node
|
return node
|
||||||
|
|
||||||
return self.parse_group()
|
return self.parse_group()
|
||||||
|
|
|
@ -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}')
|
|
|
@ -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))
|
|
|
@ -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'
|
|
|
@ -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)
|
|
|
@ -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
|
|
84
fol/unify.py
84
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
|
|
|
@ -1,13 +1,2 @@
|
||||||
import fol
|
|
||||||
|
|
||||||
if __name__ == '__main__':
|
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
|
|
||||||
|
|
Loading…
Reference in New Issue