Dustin Stevens-Baier
Comp 569- Assignment #1
Why is the MIU System called typographical?
The MIU system is typographical becuase it just a combination of movements tha are laid out in the rules, you dont have any arthimetic involved in the rules.
How does the MIU System use deduction?
The MIU system is based off four rules of inference and deduction according to Professor Wolfe's notes "implies the use of valid rules of inference," so the MIU system uses deduction by using these rules of inference. So the MIU system uses these four rules to decide what is the next step to tke towards our goal.
Does the MIU System use induction in any way? Explain.
The MIU system does not use induction becuase nothing is contingent on anything else for instance III can be replaced but it doesn't have to be replaced.
Explain any realistic interpretation of the symbols, or strings of symbols, in the MIU System.
After much contemplation (and reasearch) I found an interpretation on the web from the site
http://www.norreg.dk/tok/math01.htm
In this interpretation there are two modes M-mode and I-mode. Where M-mode is machine mode every string will start with M and only have one M given the set of rules. In my simulation I programmed a computer to geenrate as many strings in the MIU system as I deem necessary stopping only when I see the string that is desired.
I-Mode is the intellignece mode. This is when we change from just brute force to adding some human intellignece to the equation. We can start to eliminate strings that have certain sequences of characetrs in them becuase we know they will not ever meet are goal. We can actually program this in as well but the machine does no thinking and can't adapt to changes without human interaction.
Explain how conflict resolution is implemented in your simulation.
I used a brute force approach since the system was relatively small and the system could eliminate strings very fast. The conflict resolution was to randomly choose the next rule and then if that creates a string that is unusable, proceed to the next rule. Unusable was defined as a string that can be proven to be unable to create the desired MU string.
Does your implementation of the MIU System use forward or backward chaining? Explain.
My MIU System uses foward chaining becuase it starts with the string(data) and uses they four rules to work its way up to the desired goal.
The MU Puzzle: Given only the axiom MI, is MU deducible in the MIU System?
No the only using the MI axiom does not allow us to deduce MU in the MIU System. A detailed explanantion can be seen on wikipedia or a brief explantion is done by me down below.
Provide a convincing argument that MU is, or is not, deducible by the MIU System given only the axiom MI to start with.
The four rules do not allow us to create a string whose total number of Is is a multiple of three. This means that we cannot use rule three to get the MU from dropping MIII. Since the only way we can eliminate Is is by rule three and we canot add Is without adding Us in between them, we can never produce such a string.
Explain the relationship between the results of your simulation and automated theorem proving. For example, how would the computer know if it was getting closer to proving the theorem or just spinning its wheels?
My simulation had no way of telling if it was just spinning its wheels, until had had performed all the posssibilities making every string unusable as defined above. However, if one was not able to visually determine, or mathematically prove that every rule created an unsable string then the system would just continue running. this means that if we started adding other rules of Inference it could just continue looping.
