CBS6834 - Formal Ontology

This course is about formal ontology - the representation of the world in large theories coded in mathematical logic. The majority of the course will address the Suggested Upper Merged Ontology (SUMO)

Exercises

Exercise #7:

Download the E prover. Windows users can get a pre-compiled binary

To compile E on Linux, follow the instructions in the README file (slightly edited here)

tar -xzf E.tgz 
cd E
./configure
make
cd PROVER
./eprover -h | more

p(X) => q(X)
q(X)|r(X) => t(X)
p(a)

t(a) | r(a)        - conjecture

![X]:p(X) => q(X)
![X]:q(X)|r(X) => t(X)
p(a)

t(a) | r(a)        - conjecture

fof(ax1,axiom, ![X]:(p(X) => q(X))).
fof(ax2,axiom, ![X]:((q(X)|r(X)) => t(X))).
fof(ax3,axiom, p(a)).
fof(ax4,axiom, ~(t(a) | r(a) )).

/home/user/Programs/E/PROVER/eprover -auto --tptp3-format -l 2 ex.tptp 

Exercise #6:

Convert to CNF:

((((![X]:a(X))|b(X)) | (?[X]:(?[Y]:p(X,f(Y))))) <=> q(g(a),X))

Add a WordNet-SUMO mapping for kangaroo by editing the wordnet noun file. Restart Sigma and verify that it loads the new mapping. A prerequisite for this exercise is having Sigma running on your laptop. Follow the instructions in the Sigma User Guide to install Sigma

Due Oct 29

Exercise #4:

Part #1

Create an upper ontology without looking at SUMO or any other major ontology. Start with a taxonomy and English definitions. Create at least two dozen terms. Try to formalize a few axioms. Don't wait until the deadline to do this part, since there's a part #2!

Part #2

Form into groups of 2 or 3. Review each others' ontologies. Submit review comments to me.

Exercise #3:

Find appropriate "parent" terms in SUMO for the following: crater, nosh, fault line, biohazard, to peep, to thud

Represent the statements below in SUO-KIF syntax and terms from SUMO whenever possible.

• if John likes Sue then Sue likes John
• if John likes someone, that person likes him
• If Someone likes someone else then he or she has the attribute of being likable
• Every likable person knows someone
• Every human has two feet
• Every human is likable in the afternoon
• John eats with a fork

• documentation string. Maybe extract something short from Wikipedia
• termFormat expression
• subclass statement

• Create a new term and definition for "skipping" (as in "The child was skipping down the street.")
• Create a new term and definition for "bookshelf"
• Policeman
• Leeward (toward the wind)
• Being a lawyer in the US implies passing the bar exam in the state one is allowed to practice

Exercise #2:

Represent the statements below in SUO-KIF syntax. You may be able to do this just by looking at examples in the SUMO browser (type terms like "Object", "part", "Table" into the "KB term" field). You can also use the SUO-KIF manual as a reference. Also helpful may be Schaums Outlines in Logic, chapters 3 and 4, for more examples and discussion of logical representation.

• All men are mortal
• Some men are rich
• Every city has a policeman who has been beaten by every thief in the city
• In every city, each policeman has been beaten by some thief in the city
• In some cities there are policemen who have been beaten by every thief in the city

Please email your exercises to me so we can discuss them in the next class. Please make the subject field of your email "Ontology Course: Exercise #2". Feel free to ask questions!

Exercise #1:

Write a paragraph or so each on the following:

• describe any situation where two groups of people weren't communicating, due to some terminological confusion. This could consist of two groups of people using the same term or label to mean different things, or two groups using different terms to mean the same thing.
• Give an example of the symbol grounding problem in your experience
• Describe any large system of metadata in your experience
• Brainstorm on a short-term ontology-based project
  • A good default project might be adding to SUMO any terms from the standard list of Chinese radicals that do not already have an equivalent in SUMO. We may do some of these in class together.
• Start a file of terms and definitions - this is a sort of mini dictionary that will be the start for formalising terms based on SUMO. It should begin to cover terms in your proposed ontology project.

References and Resources

• The textbook for the course is Ontology: A Practical Guide .
• Much of the content of the first lecture, and some introduction of the material in subsequent lectures is covered in my on line lecture
• If at all possible, bring a laptop to class. You'll need to be online to do some of the exercises
• The Sigma browser, is a primary resource. With it you can see all the logical axioms that comprise the SUMO theory, as well as the mappings to WordNet - Sigma browser. At any time during the course, it's a good idea to get started on installing a local version of Sigma on your laptop. It's open source and can be downloaded. Installation can be a bit tricky, so we may want to schedule a lab session where I can help you get it running, but give it a try yourself first.
• Here are a few links to important parts of SUMO to help you get started thinking about the class projects.
  • The family of CaseRole(s) are relations that specify the roles of participants in Processes. An interesting project would be to expand the set of CaseRoles. In particular, the relation patient is overused, and more specialized relations are needed.
  • a link to SpatialRelation, which is a starting point for any work in regards to Casati&Varzi's Parts and Places

• A Companion to Metaphysics is a great resource. One possibility is for the student pick a very concrete topic from this encyclopedia and relate it to SUMO, with a proposed axiomatization.
• Casati and Varzi's Parts and Places appears to be out of print, but it can be ordered used from several sellers. One student project could be to read the book, and propose any axiomatizations that might not already be covered in SUMO, along with a comparison and analysis of any required differences and open issues
• Loux's Metaphysics: A Contemporary Introduction is a good source for "big" issues. A student project from this book would likely be more philosophical and less applied - an essay and not a formal axiomatization.
• WordNet If we have more students join, it would be good to have one person concentrate on issues in the SUMO-WordNet mappings, possibly sketching a concrete representation and core for the PhraseBank proposal Christiane Fellbaum and I did years ago.

This is just the list of hardcopies. I'd also expect to suggest reading of some of my application papers that are available on the web. My preference is to give each student an in-depth topic beyond my book, covering just one of the books above. So, the length of the reading list depends on the number of students joining the course, and how many professors (if any) join in as well. I'd like to be sure that we have one student tackle an axiomatization of parts and places, and the other look into an expanded axiomatization of case roles wrt SUMO, which I think is probably the most practical issue that needs addressing at the moment. It's also one that can be addressed incrementally, so can be adapted well to the time and interests of a student.

Syllabus

Project Ideas

contact: Adam Pease email, web