1. Represent the following ground facts using RDF. Note that you will need to determine how to represent non-binary relations as binary relations. You do not need to write an RDF schema. Use the basic XML syntax described on slides #182 - 192 in the large semantic web slide deck.
2. Imagine you have been hired by Amazon to make their web site part of the Semantic Web by using RDF and OWL. Your first job is do this for the Watch department.
3. The proposed Semantic Web Rule Language (described starting on slide 378) puts together ideas and syntax from OWL, Prolog, and Default Logic. A novel feature it has is the ability to assert priorities between rules. Take the example of Carlos' rules for renting an apartment that appear on slides 419-421 and determine how his first 6 rules could be written using Default Logic, i.e., without stating explicit priorities between the rules, and still support the same sets of conclusions. Describe in English why your translation works in general.
Suppose you are building a model-based system to diagnosis faults in automobiles. Following is your model of the engine (highly simplified!):
GasInTank & ~ab(FuelLine) => GasInEngine
GasInEngine & GoodSpark => EngineRuns
PowerToPlug & ~ab(SparkPlugs) => GoodSpark
PlugsInspected => ~ab(SparkPlugs)
BatteryCharged & ~ab(Cables)=> PowerToPlugs
The observations are:
~EngineRuns
GasInTank
PlugsInspected
BatteryCharged
(1) Suppose your inference engine is based on Default Logic. Show all the reasoning steps required to prove that one diagnosis is {ab(FuelLine)} and the other diagnosis is {ab(Cables)}.
(2) Suppose your inference engine is based on Circumscription. Show all the reasoning steps required to prove that the sentence:
ab(FuelLine) v ab(Cables)
is true in all models of Model U Observations that are minimal with respect to ab.
Written exercises:
1. Find all resolvents of the following pairs of clauses:
{P (x, y), P (y, z )}, {¬P (u, f (u))}
{P (x, x), ¬R(x, f (x))}, {R(x, y), Q(y, z )}
{P (x, y), ¬P (x, x), Q(x, f (x), z )}, {¬Q(f (x), x, z ), P (x, z )}
{P (x, f (x), z ), P (u, w, w)}, {¬P (x, y, z ), ¬P (z , z , z )}
2. Consider the following information:
1. Animals can outrun any animals that they can eat.
2. Carnivores eat other animals.
3. Outrunning is transitive: if x can outrun y and y can outrun z, then x can outrun z.
4. Lions eat zebras.
5. Zebras can outrun dogs.
6. Dogs are carnivores.
Translate these assertions into FOL CNF. By hand, create resolution refutation proofs using answer extraction to find three animals that lions can outrun.
3. Using one of the methods for reasoning with equality discussed in class (that is: adding extra axioms, using equivalence classes, or paramodulation), create by hand a resolution-refutation proof that the solution to the riddle, "Brothers and sisters have I none, but that man's father is my father's son" is "that_man = me".
4. "Schubert's Steamroller" (named after Len Schubert) is a test problem for automated theorem proving which can be stated as follows:
Wolves, foxes, birds, caterpillars, and snails are animals, and there are some of each of them. Also, there are some grains, and grains are plants. Every animal either likes to eat all plants or all animals much smaller than itself that like to eat some plants. Caterpillars and snails are much smaller than birds, which are much smaller than foxes, which in turn are much smaller than wolves. Wolves do not like to eat foxes or grains, while birds like to eat caterpillars but not smails. Caterpillars and snails like to eat some plants.
Therefore, there is an animal that likes to eat a grain-eating animal.
Translate this problem into Prover9's input notation, and use it find a proof. Turn in your formulation and the output from the prover. Note: because this is a well known problem, you will be able to find translations of it online. But please do not look at the other versions until you try your own!
5. Optional, for extra credit: find a mathematical theorem from a textbook that you have used in a mathematics class that you can translate into FOL and prove using Prover9.
Here are the files we discussed in class for parsing and interpreting sentences about Adam and Eve:
Expand genesis_semantics.pl so that it handles:
For sentences that are syntactically ambiguous, print out all the different parses by using the ";" after each is printed
At the command line of your favorite computer, try invoking prolog. If it is not installed, then download and install SWI-PROLOG in your home directory. Define and test the following predicates:
Research the rules regarding who is a US citizen. Determine a set of predicates and functions needed to represent this domain. Write a set of formulas in first order logic that axiomatize citizenship. Present two examples of how your axioms could be used to prove the citizenship of particular indivduals, by specifying a set of facts about the individual and performing a resolution-refutation proof. Turn in the first draft of your solution on Oct 14, and the final version on Oct 16. Your solution should be typed except for the resolution proofs, which may be hand written. Use regular infix notation rather than LISP notation. Your axioms do not need to be in CNF, but note that you may need to convert some of them to CNF if you want to use them in your example proofs. To represent the "for all" sign (upside down A) you should just type capital A, and similarly type capital E for the "exists" sign. Use v, &, ~, =>, and == for or, and, not, implies, and equivalent respectively. In terms of precedence, ~ comes first, then v and &, next => and ==, and finally the quantifiers. For example,
A x animal(x) & large(x) & ~imaginary(x) => elephant(x) v whale(x)
is the same as:
A x ((animal(x) & large(x) & (~imaginary(x))) => (elephant(x) v whale(x)))
Every student should implement and turn in his or her own solution. However: on this assignment, you are encouraged to collaborate informally: talk with each other about work, share ideas and techniques. Feel free to look on the Web for examples of other solutions to similar problems which you can adapt. In other words, anything goes in terms of you figuring out how to solve the problem, but at the end of the day I'd like you to type up your own solution. You will turn in the code for your solution together with a short note citing what resources (people, books, and/or Web sites) you used. You should email your solution as an attachment to the TA Carlos by Thursday, Oct 2nd.
We will check the correctness of your solution by running it on our own test data. Before you turn in your solution, you should test your solution on examples that you make up yourself. Testing is also a good time to collaborate with your fellow students. Note that it is possible that two solutions that produce different output are both correct, if the outputs are logically equivalent.
There are different projects for the undergraduates and the graduate students:
(OR (NOT (OR P (NOT Q))) R S)
your program might output
(OR G1 R S)
(OR (NOT G1) G2)
(OR (NOT G2) (NOT P))
(OR (NOT G2) Q)
where G1 and G2 are new propositions created using the GENSYM function. Your solution should include a function that we will use to test it:
(convert-to-cnf input-file output-file)
The function takes two string arguments, the names of an input and output file.
(convert-to-cnf-schema input-file output-file)
The function takes two string arguments, the names of an input and output file.
This assignment should be done in teams of 2 or 3 students. Turn in only one copy of the solution. Your solution should be typed. You should be sure to keep a copy of the file containing your solution, because you will need it again. You should allow yourself 3 hours to complete this assignment.
A cryptarithmetic problem uses up to 10 letters to represent distinct numerals. The problem is to find an assignment of the letters to numerals that satisfies a given arithmetic problem.
Your assignment is to come up with a set of clause schemas that represent the problem: DAN + NAN = NORA. You should NOT solve the problem by hand, and then simply write down a set of clauses that represent the solution. Instead, you should create a set of clauses that directly represents the unsolved problem, such that any model of the clauses corresponds to a solution. You will then run your schemas through our schema interpreter, use a SAT engine to solve the problem, and verify that the solution to the SAT problem corresponds to a solution to the original cryptarithmetic problem.
See the BNF syntax for propositional schemas. Note that an mathematical expression involving variables can appear as an argument to a predicate. This is okay because such an expression can be evaluated when the clause schema is expanded. For example, if a proposition such as (A 5) is used to mean "A is assigned the numeral 5", then in a schema where X and Y are integer valued (range) variables, a literal such as (A (+ X Y)) may appear.
Hint: first work out an encoding that does not allow "carrying the one". Then, generalize it to the full solution.
On September 11: bring your first-draft solution to class.
On September 18: turn in: