Programming assignment 3
The final programming assignment is to write a tableau based ALC reasoner without general TBoxes or non-empty ABoxes. You will define two interface functions:
def satisfiable(concept, tbox={}):
"""This function takes a concept expression "parse tree" as
specified (e.g., as a collection of nested tuples, plus an option
TBox (encoded as a dictionary of strings/concept expressions), and
returns True if the concept expression is satisfiable given the
TBox, and False if not."""
pass
def subsumed(subsumed, subsumer, tbox={}):
"""This function takes two concept expressions and returns True iff
the subsumed isSubclassOf subsumer given the TBox."""
pass
You will also submit three "interesting" ALC examples. If I can get the RDF2InternalFormat working they will be in a new species of OWL called OWL-ALC. Otherwise, they will be in the concept expression format. The examples may use TBoxes, and they may share them. The first example is due on Wednesday, April 28, class time. The second two are due on Monday, May 3, class time. The reasoner is due on May 12th, Hawaii time.
Submission is the usual thing. For each example, the subject line should be [CMCS498w]Example 1 (or 2, or 3, as apropriate). The attachement should be yourInitials_ex1.py (or 2, 3). There should be, among whatever else you have in there, two variables 'tbox' and 'concept', filled with the obvious things.
The Concept Expression format
The concept expression format is simple:
- Atomic class names are arbitrary Python strings, e.g., "foo", "a", "Person", "http://www.example.org/#Test"
- There is a disjoint set of strings which form the property names, e.g., "p", "accross", "enamouredOf"
- Negation/complementOf is expressed with a binary tuple whose first element is the string "not", and whose remaining element is a concept expression, e.g., ("not", "C")
- Conjunction/intersectionOf and disjunction/unionOf are expressed with tuples of length greater than one whose first element is the string "and" or "or", respectively, and whose remaining elements are concept expressions, e.g., ("or", ("not", "well-liked"), "friendly", "amiable")
- Universal/allValuesFrom and existential/someValuesFrom quantification is expresse with trinary tuples whose first element is "all" or "some", respectively, whose second element is a property name, and whose third element is a concept expression, e.g., ("some", "hasChild", ("and", "happy", "female")).
Some examples:
("and", "Person", ("not", "female"))
("all", "hasNeighbor",
("or", "loud", "noisy", "pyscho"))
("some", "hasFriend",
("some", "likes", ("or", "Sport", "Dance"))
The TBox
The TBox is encoded as a dictionary with strings (class names) as the keys and tuples (concept expression parse trees) as the values. TBoxes will be unfoldable (in particular, non-cyclic).
An example (roughly from page 56 of DLHB):
{'Woman': ('and', 'Person', 'Female'),
'Man': ('and', 'Person', ('not', 'Female')),
'Mother': ('and', 'Woman', ('some', 'hasChild', 'Person')),
'Father': ('and', 'Man', ('some', 'hasChild', 'Person')),
'Parent': ('or', 'Mother', 'Father'),
'GrandMother': ('and', 'Mother', ('some', 'hasChild', 'Person')),
'MotherWithoutDaughter': ('and', 'Mother', ('all', 'hasChild', ('not', 'Woman'))),
'Wife': ('and', 'Woman', ('or', ('some', 'hasHusband', 'Man'),('some', 'hasWife', 'Woman')))}
This is a bit of a pain to type. Here's how I simplify the typing:
#This bit will declare eponyous module variables with
#the various string values. It's up to me to make sure I use them correctly.
#"and", "or" and "not" are keywords, so I have to do something special
#for them (see below)
conj = "and"
disj = "or"
neg = "not"
some = "some"
all = "all"
# All the class names I'm going to use.
names = ['Woman', 'Person', 'Female',
"Man", "Father", "Parent", "GrandMother", "Mother",
"MotherWithoutDaughter", "Wife"]
# All the properties. Not that it makes a difference to keep them separate, but it's
# convenient and helps me, the author, keep track.
names += ['hasChild', 'hasHusband, 'hasWife']
# Add all the names to the current module namespace.
for i in names:
globals()[i] = i
# This is the same tbox as above.
tbox = {Woman: (conj, Person, Female),
Man: (conj, Person, (neg, Female)),
Mother: (conj, Woman, (some, hasChild, Person)),
Father: (conj, Man, (some, hasChild, Person)),
Parent: (disj, Mother, Father),
GrandMother: (conj, Mother, (some, hasChild, Person)),
MotherWithoutDaughter: (conj, Mother, (all, hasChild, (neg, Woman))),
Wife: (conj, Woman, (disj, (some, hasHusband, Man), (some,
hasWife, Woman)))}
# Displays the tbox with full quoting.
print tbox
The Reasoner
Recall that in order to use a tableau, you must put concepts in negation normal form (NNF), empty the TBox, and then put the concept expression you are testing on a fresh individual (a.k.a., node), and apply the expansion rules until 1) you have an or-branch that is clash free and the rules can no longer be applied, or 2) there is a clash on every or-branch.
I presume y'all can figure out NNF.
ALC has four expansoin rules (see the first four rules on page 85 of the DLHB. I restate them here, using nodes and edges instead of ABoxes to describe the rules (in what follows, p is a property name, while C and D are concept expressions):
| Rule name | Condition | Action |
| and-rule | The label of some node X contains ("and", C, D, ...), but doesn't contain any one of the conjuncts | Add the conjuncts to the label of X |
| or-rule | The label of some node X contains ("or", C, D, ...), but doesn't contain any of the disjuncts | Make a clone of the tree for each disjunct, add the respective disjunct to the respective clone of the label of X |
| all-rule | The label of some node X contains ("all", p, C), and node X is connected by a edge labeled with p to some node Y, and Y's label doesn't contain C | Add C to Y's label |
| some-rule | The label of some node X contains ("some", p, C), and there is no p-edge from X to a node, Y, such that Y's label contains C | Create new node, Z, whose label contains C, and add an edge labeled "p" from X to Z |
A clash occurs in a tree just in case there is some node's label that contains an atomic concept and its negation. A tree is complete if no more rules apply. If any tree is complete, then the original concept is satisfiable. If all trees contain a clash, the original concept is unsatisfiable.
Some advice
Do not work directly with the concept expression language. Instead
use it to construct your own objects. For example, you could
imagine NNF working directly on the tuples: As we discussed in class, this was
NOT good advice! Necessarily. What you *really* want to avoid is
implementing node labels as lists of concept expressions.
from types import *
def nnf(wff):
if type(wff) == StringType:
return(wff)
...
test = nnf("A")
#returns "A", as it should
For NNF, this can work ok, but once you start building the tree, you'll want to cluster your conjunctions, atomics, etc., and avoid testing rule-applicability for concepts you've already fired on. This was the good part of the advice :)
Per Rafi's question...building up a big class heirarchy just for the concept expression is silly *unless* you have a much cleverer representation. If you just make a class that has a connective and a list of arguments... you've not gained anything.
You can unfold your TBox up front, but you ought to do lazy unfolding.
Test first, early and often. There's a good unit testing frame work. Start with NNF. Get clash detection working early. The and and all rules are very easy, and easy to test. Get them working and make a complete end to end reasoner working with just them.
The or-rule requires backtracking. Cloning will work, but it won't be hard to make it prohibitively expensive. Experiment with different backtrack/restore schemes.
You should think about the rules. They aren't stated witha particular eye to direct implementation (though you could implement them directly). Take the and-rule. It says that if any conjunct is missing, you should add all of them. Don't do that
Extra Credit
Extend your reasoner to handle ALN. Process your (perhaps modified) pizza ontology.