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

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
Create a file with the following inference test for E:

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

t(a) | r(a)        - conjecture
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) ))).
Here are some command line invocations for Linux to run the prover and process the proof
/home/msmith/Programs/E/PROVER/eprover -xAuto -tAuto --tptp3-in -l 4 ex.tptp > out.tptp
/home/apease/Programs/E/PROVER/epclextract out.tptp
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

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