Due: Feb 23th, 2010 at 11:59PM
1. Objectives and Overview
In this exercise you will practice writing semantic representations of natural language utterances in first-order logic. You will also gain experience with using event semantics. Furthermore, to show that your formulas are well formed, you will also be asked to use an automated theorem prover.
2. Reference files
The reference files for this assignment are:
3. Detailed instructions
Task 0:
Prepare for the assignment by reading 17–17.4 in J&M, and sections 10–10.3 of the NLTK book.
Task 1:
Using sentences.fol as a reference, create by hand a file called forumulas.fol that contains semantic representations (using event semantics) of each of the sentences in sentences.fol. You may simply add the semantic representation after each commented sentence. To check to see whether your formulas are well-formed, we will use this code to read your formulas.fol. That is, YOU do not need to write any code for this assignment, just the formulas.
Task 2:
Next, using sentences.prover as a reference, create by hand a file called forumulas.prover that looks like this and contains semantic representations (using event semantics) of the sentences. The goal is to use a theorem prover to prove the goal of each set of sentences. We will use this code to read in your formulas and do the proofs. Each goal should return TRUE.
4. Running your code
YOU DO NOT NEED TO WRITE ANY CODE FOR THIS ASSIGNMENT, ONLY FORMULA FILES.
5. How to turn in your work
Turn in your assignment using CollectIt. Please TAR your files and name the tar’d file with the extension .tar. Please don’t use ZIP, tar.gz, gzip, rar, etc.
Use the filename of whatever homework we’re on, e.g. for homework 6 name your file hw6.tar. Yes you will all have the same filename for your homeworks, but this doesn’t matter because of the way that CollectIt handles things.
To tar (available on Patas) from the directory that your work is in:
$ tar -cvf hw6.tar *
6. Assessment
This homework is worth 10% of your total grade. Assessment criteria are explained here.