Questions to email@example.com
Last modified: May 11, 1999.
Below, the answers to the most frequent questions about the FANs project.
Determining the inconsistency of rule sets (what do theorem provers
have to do with this anyway?)
If you are programming in C, you can use the theorem prover Otter to determine whether a set of sentences is inconsistent. In general, a theorem prover determines whether a conclusion follows from a set of premises by checking whether the premises together with the negation of the conclusion are inconsistent. If so, the theorem is proved.
In fact, when Otter checks to see if a conclusion follows from a set of premises, it expects the conclusion to be negated. Then it just checks the set for inconsistency. We can use this fact to check whether a set of sentences is inconsistent. You pass it a set of sentences, as if to ask Otter if the last sentence follows from the other premises. Otter will check the set for inconsistency. If it finds inconsistency, it will say that the theorem is proved. If it doesn't find inconsistency, it reports that it has exhausted its search space. Someone trying to prove a theorem can infer that probably the fact he or she is trying to prove is not a theorem; in our case, we can infer that the set of sentences is most likely consistent. (Remember that checking for inconsistency, or equivalently, checking whether a conclusion follows from a set of premises, is only semi-recursive.)
CORRECTION: Please note that one does not have to negate the last (or any) sentence in the set one passes to Otter, because Otter already expects negation.
The code that Stathis provided is not quite the black box that was originally promised, but is hopefully close enough. You will have to fix several things: The version previous to today negated the last sentence; just get rid of that part. YOu probably want to have the code return a boolean value depending on whether or not the output file contains the string "That finishes the proof of the theorem" , meaning inconsistency of your set. You will also need to modify the code to have the code read from other files or other data structures, etc. If you have further questions about this, please contact Stathis or me.
Forms of input. What will the files be like? What
size assumptions can be made? Can they be modified
manually? When will the final input files be available?
There are currently samples on the web of the net input file and the rules input file. The net input file may change slightly, but will be about this size. The rules input file will be considerably longer. However, both files will remain the same in format.
You can safely assume that there won't be more than a few hundred nodes; that the depth of the network won't be more than 5 or 6; that no node will have more than 10 rules attached.
Final input files will be available in a few days. If you want to change them manually, that's fine; however, please include the modified file as part of the project and explain what you have done.
If a node has multiple supertypes, and there are no numbers provided
after the supertypes, there are two cases:
1. The nodes are not themselves organized in a hierarchy. That is, for each pair of supertypes a and b, it is not the case either that a is a supertype of b, or that b is a supertype of a. In this case, you can assign any order you want.
2. Some of the nodes are organized in a hierarchy. That is, there are some nodes where it can be determined from the structure of the network that one is a supertype of another. In this case, the preference ordering of specificity applies. Remember, you only need consider an ordering on supertypes when doing rules inheritance. The rules inheritance process follows the FAN preprocessing step (Stein's algorithm), in which it is determined, for any pair of nodes, if one is more specific than another.
How should the program run? Using an interactive interface?
A command line interface? Something else?
It's really your choice. It would be very nice to have an interactive interface. A command line interface would also be nice. These aren't strictly necessary, however, and I'll be satisfied with a program that can sequentially read commands from an input file, and provide the answers. The point of this assignment is not dealing with a lot of input and output issues. In a few days, I will give you a list of queries that I would like your program to be able to answer. Examples of such queries are:
Do you want comments or a README file?
Absolutely, yes to both. Comments are essential, and good prose does count in the grading process.
Back to web page for KR course