Compare commits
2 Commits
badb08ec05
...
bfd64b20b6
Author | SHA1 | Date |
---|---|---|
bog | bfd64b20b6 | |
bog | fb41410797 |
|
@ -1 +1,2 @@
|
||||||
__pycache__
|
__pycache__
|
||||||
|
*.prof
|
|
@ -0,0 +1,5 @@
|
||||||
|
.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 ::= NOT | opar F cpar
|
GROUP ::= PRED | opar F cpar
|
||||||
PRED ::= pred opar TERM (comma TERM)* cpar
|
PRED ::= pred opar TERM (comma TERM)* cpar
|
||||||
|
|
||||||
TERM ::=
|
TERM ::=
|
||||||
|
|
|
@ -1,5 +1,13 @@
|
||||||
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):
|
||||||
|
@ -8,3 +16,11 @@ 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
|
||||||
|
|
|
@ -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
|
|
@ -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()
|
10
fol/lexer.py
10
fol/lexer.py
|
@ -66,7 +66,10 @@ class Lexer:
|
||||||
cursor = self.cursor
|
cursor = self.cursor
|
||||||
value = ''
|
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]
|
value += self.text[cursor]
|
||||||
cursor += 1
|
cursor += 1
|
||||||
|
|
||||||
|
@ -80,7 +83,10 @@ class Lexer:
|
||||||
cursor = self.cursor
|
cursor = self.cursor
|
||||||
value = ''
|
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]
|
value += self.text[cursor]
|
||||||
cursor += 1
|
cursor += 1
|
||||||
|
|
||||||
|
|
|
@ -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
|
|
@ -1,26 +1,4 @@
|
||||||
class Node:
|
from fol.node import 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:
|
||||||
|
@ -114,7 +92,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_pred())
|
node.add_child(self.parse_group())
|
||||||
return node
|
return node
|
||||||
|
|
||||||
return self.parse_group()
|
return self.parse_group()
|
||||||
|
|
|
@ -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}')
|
|
@ -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))
|
|
@ -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'
|
|
@ -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)
|
|
@ -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
|
|
@ -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
|
|
@ -1,2 +1,13 @@
|
||||||
|
import fol
|
||||||
|
|
||||||
if __name__ == '__main__':
|
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
|
||||||
|
|
Loading…
Reference in New Issue