CBS6834 - Formal Ontology

Exercises | References | Syllabus | Project Ideas

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 9 (done in class)

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
You'll create a file with the following inference test for E, which is presented simplified first here:

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

t(a) | r(a)        - conjecture
TPTP languages require all quantifiers to be explicit though:
![X]:p(X) => q(X)
![X]:q(X)|r(X) => t(X)
p(a)

t(a) | r(a)        - conjecture
And the actual test file requires some syntactic "wrappers" around the formulae

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) )).
Save this file as ex.tptp. Run the following command line invocation (changing the path to eprover as needed in your installation) for Linux to run the prover and generate a proof.
/home/user/Programs/E/PROVER/eprover -auto --tptp3-format -l 2 ex.tptp 

Can you follow the proof and see why a contradiction follows from the four formulas in the input? You can get many more test problems from the TPTP

Exercise #6:

Convert to CNF:

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

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.

Create a very basic definition for kangaroo, consisting of at least the following statements in SUO-KIF and SUMO, paying careful attention to strictly correct syntax.

The following are harder, and may be considered "extra credit"

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.

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:

Please email your exercises to me. Please make the subject field of your email "Ontology Course: Exercise #1". Feel free to ask questions!

References and Resources

Books

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

Please note that this is subject to change based on Prof. Huang's guidance.

Project Ideas

contact: Adam Pease email, web