234 lines
8 KiB
Python
234 lines
8 KiB
Python
from emis_funky_funktions import *
|
|
|
|
from itertools import combinations, product
|
|
from operator import eq
|
|
from typing import Collection, FrozenSet, TypeAlias
|
|
|
|
from ir import Clause, Clause_, IRNeg, IRProp, IRTerm, IRVar, KnowledgeBase, KnowledgeBase_, Substitutions, sub_all, unify
|
|
|
|
def terms_cancel(t1: IRTerm, t2: IRTerm) -> Option[Substitutions]:
|
|
"""
|
|
Determine if two terms could cancel each other out, given the right substitutions
|
|
|
|
That is, is there some set of substitutions such that t1 = ¬t2 or ¬t1 = t2?
|
|
|
|
If negation is possible and a substitution exists, that substitution is returned.
|
|
Otherwise, `None` is returned.
|
|
|
|
>>> terms_cancel(IRNeg(IRVar('x1')), IRProp('Terezi'))
|
|
Some((Terezi()/x1,))
|
|
|
|
>>> terms_cancel(IRProp('Nepeta'), IRVar('x1'))
|
|
Some((¬Nepeta()/x1,))
|
|
|
|
>>> terms_cancel(IRProp('ancestor', [IRVar('x1')]), IRVar('x1')) is None
|
|
True
|
|
"""
|
|
match (t1, t2):
|
|
case (IRNeg(a), b) | (b, IRNeg(a)): #type: ignore
|
|
return hush(unify(a, b))
|
|
case (IRVar(_) as x, a) | (a, IRVar(_) as x): #type: ignore
|
|
return hush(unify(x, IRNeg(a)))
|
|
return None
|
|
|
|
def merge_clauses(c1: Clause_, c2: Clause_) -> KnowledgeBase:
|
|
"""
|
|
Produce a list of all possible clauses which resolution could derive from c1 and c2
|
|
|
|
For each term in c1 that could cancel with a term in c2 using a substitution, a
|
|
possible clause is produced equal to the union of c1 and c2 with the canceled
|
|
terms removed and the substitution applied.
|
|
|
|
>>> merge_clauses(
|
|
... [ IRProp('day'), IRNeg(IRProp('night')) ],
|
|
... [ IRProp('night') ]
|
|
... )
|
|
{ { day() } }
|
|
|
|
>>> merge_clauses(
|
|
... [ IRNeg(IRProp('transgender', [IRVar('x1')])), IRProp('powerful', [IRVar('x1')]) ],
|
|
... [ IRNeg(IRProp('powerful', [IRVar('x2')])), IRProp('god', [IRVar('x2')]) ]
|
|
... )
|
|
{ { god(*x1), ¬transgender(*x1) } }
|
|
|
|
>>> merge_clauses(
|
|
... [ IRNeg(IRProp('day')), IRProp('night') ],
|
|
... [ IRVar('x2') ]
|
|
... )
|
|
{ { night() }, { ¬day() } }
|
|
|
|
If two clauses cannot merge, an empty set is returned
|
|
|
|
>>> merge_clauses(
|
|
... [ IRProp('day') ],
|
|
... [ IRProp('wet') ]
|
|
... )
|
|
{ }
|
|
"""
|
|
terms1, terms2 = list(c1), list(c2)
|
|
valid_substitutions = drop_none(
|
|
map_opt(lambda subs: (subs, i1, i2), terms_cancel(t1, t2))
|
|
for ((i1, t1), (i2, t2)) in product(enumerate(terms1), enumerate(terms2))
|
|
)
|
|
return FSet(
|
|
FSet(
|
|
sub_all(subs, term)
|
|
for term in (*terms1[:i1], *terms1[i1 + 1:], *terms2[:i2], *terms2[i2 + 1:])
|
|
)
|
|
for (subs, i1, i2) in valid_substitutions
|
|
)
|
|
|
|
def derive(clauses: KnowledgeBase_) -> KnowledgeBase:
|
|
"""
|
|
All possible clauses which derive in one step of resolution from a knowledge base
|
|
|
|
Attempts to merge every possible combination of clauses, in the knowledge base.
|
|
|
|
>>> derive([
|
|
... [IRNeg(IRProp('animal', [IRProp('Kim')]))],
|
|
... [IRNeg(IRProp('dog', [IRVar('x0')])), IRProp('animal', [IRVar('x0')])],
|
|
... [IRNeg(IRProp('cat', [IRVar('x1')])), IRProp('animal', [IRVar('x1')])],
|
|
... [IRProp('dog', [IRProp('Kim')])],
|
|
... ]) #doctest: +NORMALIZE_WHITESPACE
|
|
{
|
|
{ animal(Kim()) },
|
|
{ ¬cat(Kim()) },
|
|
{ ¬dog(Kim()) }
|
|
}
|
|
"""
|
|
return FSet(
|
|
FSet(clause)
|
|
for (c1, c2) in combinations(clauses, 2)
|
|
for clause in merge_clauses(c1, c2)
|
|
)
|
|
|
|
def derive2(kb1: KnowledgeBase_, kb2: KnowledgeBase_) -> KnowledgeBase:
|
|
"""
|
|
All clauses which derive in one step from the combination of two knowledge bases
|
|
|
|
Each resulting clause is the combination of one clause from the left knowledge base
|
|
with exactly one clause from the right knowledge base. Clauses from the same
|
|
knowledge base will not be combined.
|
|
|
|
>>> derive2([
|
|
... [IRNeg(IRProp('animal', [IRProp('Kim')]))],
|
|
... [IRNeg(IRProp('cat', [IRVar('x1')])), IRProp('animal', [IRVar('x1')])],
|
|
... ], [
|
|
... [IRNeg(IRProp('dog', [IRVar('x0')])), IRProp('animal', [IRVar('x0')])],
|
|
... [IRProp('dog', [IRProp('Kim')])],
|
|
... ])
|
|
{ { ¬dog(Kim()) } }
|
|
"""
|
|
return FSet(
|
|
FSet(clause)
|
|
for (c1, c2) in product(kb1, kb2)
|
|
for clause in merge_clauses(c1, c2)
|
|
)
|
|
|
|
false_clause: Clause = FSet()
|
|
"""
|
|
The clause which represents the logical condition False
|
|
|
|
i.e. the empty clause
|
|
"""
|
|
|
|
|
|
def next_generation(
|
|
previous_generations: KnowledgeBase_,
|
|
current_generation: KnowledgeBase_,
|
|
) -> KnowledgeBase:
|
|
"""
|
|
Advance resolution by one step
|
|
|
|
This performs `derive()` on the current generation as well as `derive2()` between the
|
|
current generation and all clauses from previous generations in order to produce a new
|
|
generation, hopefully with new and interesting clauses in it.
|
|
|
|
When using the new generation, previous generations should be considered to be the sum
|
|
of all clauses within the two knowledge bases passed to this function. That is, all
|
|
clauses which were used in the generation of that generation.
|
|
|
|
### Example
|
|
|
|
Starting from an example knowledge base, we produce a new generation. Notice that the
|
|
empty list for previous generations indicates that this is the zeroth (original)
|
|
knowledge base.
|
|
|
|
>>> next_generation([
|
|
... ], [
|
|
... [IRNeg(IRProp('animal', [IRProp('Kim')]))],
|
|
... [IRNeg(IRProp('dog', [IRVar('x0')])), IRProp('animal', [IRVar('x0')])],
|
|
... [IRNeg(IRProp('cat', [IRVar('x1')])), IRProp('animal', [IRVar('x1')])],
|
|
... [IRProp('dog', [IRProp('Kim')])],
|
|
... ]) #doctest: +NORMALIZE_WHITESPACE
|
|
{
|
|
{ animal(Kim()) },
|
|
{ ¬cat(Kim()) },
|
|
{ ¬dog(Kim()) }
|
|
}
|
|
|
|
Now, we perform the next round of resolution. All of the terms originally passed into
|
|
the first generation have been moved to the previous generations knowledge base, and
|
|
the current generation contains only the results from the first call.
|
|
|
|
>>> next_generation([
|
|
... [IRNeg(IRProp('animal', [IRProp('Kim')]))],
|
|
... [IRNeg(IRProp('dog', [IRVar('x0')])), IRProp('animal', [IRVar('x0')])],
|
|
... [IRNeg(IRProp('cat', [IRVar('x1')])), IRProp('animal', [IRVar('x1')])],
|
|
... [IRProp('dog', [IRProp('Kim')])],
|
|
... ], [
|
|
... [IRNeg(IRProp('dog', [IRProp('Kim')]))],
|
|
... [IRNeg(IRProp('cat', [IRProp('Kim')]))],
|
|
... [IRProp('animal', [IRProp('Kim')])],
|
|
... ])
|
|
{ { } }
|
|
|
|
The return of a knowledge base containing false (ie `[]`) indicates that resolution
|
|
has found a contradiction. In this case, there are two: One from ¬dog(Kim) and
|
|
dog(Kim), and one from animal(Kim) and ¬animal(Kim).
|
|
"""
|
|
return fset(*derive(current_generation), *derive2(current_generation, previous_generations))
|
|
|
|
def derives_false(
|
|
knowledge_base: KnowledgeBase,
|
|
previous_generations: KnowledgeBase = FSet(),
|
|
) -> bool:
|
|
"""
|
|
Determine if it is possible to derive false from a given knowledge base.
|
|
|
|
Uses any number of generations of resolution via `next_generation()` to find a
|
|
generation which contains the `false_clause`, indicating that the original knowledge
|
|
base (and all subsiquent generations) are contradictory.
|
|
|
|
`previous_generations` may be set if the current knowledge base was derived from some
|
|
other series of clauses using `derive()`.
|
|
|
|
>>> derives_false(fset(
|
|
... fset( IRNeg(IRProp('animal', (IRProp('Kim'),))) ),
|
|
... fset( IRNeg(IRProp('dog', (IRVar('x0'),))), IRProp('animal', (IRVar('x0'),)) ),
|
|
... fset( IRNeg(IRProp('cat', (IRVar('x1'),))), IRProp('animal', (IRVar('x1'),)) ),
|
|
... fset( IRProp('dog', (IRProp('Kim'),)) ),
|
|
... ))
|
|
True
|
|
|
|
>>> derives_false(fset(
|
|
... fset( IRNeg(IRProp('animal', (IRProp('Kim'),))) ),
|
|
... fset( IRNeg(IRProp('dog', (IRVar('x0'),))), IRProp('animal', (IRVar('x0'),)) ),
|
|
... fset( IRNeg(IRProp('cat', (IRVar('x1'),))), IRProp('animal', (IRVar('x1'),)) ),
|
|
... ))
|
|
False
|
|
"""
|
|
if false_clause in knowledge_base:
|
|
return True
|
|
elif len(knowledge_base) == 0:
|
|
return False
|
|
else:
|
|
return derives_false(
|
|
next_generation(previous_generations, knowledge_base),
|
|
knowledge_base | previous_generations
|
|
)
|
|
|
|
|
|
if __name__ == '__main__':
|
|
import doctest
|
|
doctest.testmod() |