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)

Participants (who get book copies): Xu Jian*, Francesca QUATTRI*, Yan JIANG*, Michal SVARNY*, Jiajia LI*, Hongzhi XU*

Additional book copies for: Chu-Ren HUANG*, Grace NGAI*, Qin LU*, Huarui ZHANG*, Jing DING*, Shan WANG*, Jingxia LIN, LEE Yat-mei (Sophia)*, Yao Yao*
an * denotes that I've delivered a book to you


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
./eprover -h | more
You'll create a file with the following inference test for E:

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

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

fof(ax1,axiom, (p(X) => q(X))).
fof(ax2,axiom, ((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 -xAuto -tAuto --tptp3-in --tptp3-out -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

Completed in class by: Michal, Prof. Jiang, Hongzhi, Francesca, HuaRui

Exercise #6:

Convert to CNF:

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

Due Nov 12

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.

Due: Oct 29

Completed so far by:

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"

Completed so far by: Michal, Francesca, Prof Jiang, Jiajia, XU Jian

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 by October 7 so we can discuss them in the next class. Please make the subject field of your email "CBS6834: Exercise #2". Feel free to ask questions!

Completed so far by: Prof Jiang, Jiajia, Michal, Francesca, XU Jian

Exercise #1:

Write a paragraph or so each on the following:

Please email your exercises to me by September 23 so we can discuss them in the next class. Please make the subject field of your email "CBS6834: Exercise #1". Feel free to ask questions!

Completed so far by: Francesca, XU Jian, Jiajia, Michal

References and Resources


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.


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

Project Ideas

contact: Adam Pease email, web