Here it is! ==> *** RUN IT ***
This program is just a sort of calculator that has operations like Uniform Substitution and Modus Ponens as basics.
Various changes made 16apr2001 to fix MP search problems.
It is up and running, but without assumption and discharge, or specific rules for dealing with quantifiers.
Substitution is aware of quantifiers, bound and free variables, and won't accept substitutions that capture free variables as bound.
I'm still open for user interface suggestions on how you state WHICH quantifier in an expression a bound variable renaming should apply to. This is being a stumbling block on implementing UG and related rules.
There is no code for definitions... Nor am I sure what form they should take. The user interface issues are very much the same ones as with quantifier rules.
The Modus Ponens code is still using search in a few cases where it should be doing hashes.
The Necessatation code now puts the correct line number in the justification.
The core is a CGI program written in Perl. *SOURCES*
Notations are read from a file, so the calculator can handle alternate notations.
There is some minimal documentation on Notations.
The logic systems are read from a file, so that the calculator can handle alternate systems.
There is some minimal documentation on Systems.
When doing proofs, the number of possible cases can sometimes explode dramaticly. Unfortunately programs dealing with this often follow suit.
THEREFORE: I have made a number of simplifying assumptions which help to cut down on the problem. (Hopefully none of them will cause me any problems later.)
A given result may appear ONLY ONCE in the currently active (Non-discharged) proof. Any reference to the second one could be mapped to a reference to the first one without loss of generality or complication.
When theorems are looked up, they are first reduced to a connonical form. This form differs from the original only in renaming of variables. This allows a fast [hashed] lookup to be done, instead of having to search through all the stored theorems.
The storage form of an expression is LISP style notation such as:
(IMP (IMP p q) (EXISTS x (IMP p q)))
This form is converted into trees inside the program and most routines walk those trees.
The program first gives a welcome screen, and requires the user to select a notational system. This enables the user to see the later steps (such as selecting an axiom system) in the notation of her choice.
The program then gives the user a chance to select an Axiom System to use as a basis for the proof.
The program then allows the user to state a proof goal. This is optional, but if the goal is stated the program may be able to provide some suggestions later.
Currently no natural deduction proofs can be done. (Code to handle assumptions and discharges not functional yet.)
Each step that can be taken at a given point has a Button or Link that takes that step.
An example output derivation is: (CS notation, default system)
1: p>(q>p) Axiom A1 2: (p>(q>r))>((p>q)>(p>r)) Axiom A2 3: p*q>p Axiom A3 4: p*q>q Axiom A4 5: p>(q>p*q) Axiom A5 6: p>p+q Axiom A6 7: q>p+q Axiom A7 8: (p>r)>((q>r)>(p+q>r)) Axiom A8 9: (p==q)>(p>q) Axiom A9 10: (p==q)>(q>p) Axiom A10 11: (p>q)>((q>p)>(p==q)) Axiom A11 12: (-p>-q)>(q>p) Axiom A12 Stated Goal: (p*q>p)*(p*q>q) 13: (p*q>p)>((p*q>q)>(p*q>p)*(p*q>q)) 5,US,p*q>p/p, p*q>q/q 14: (p*q>q)>(p*q>p)*(p*q>q) 3,13,MP 15: (p*q>p)*(p*q>q) 4,14,MP
I'm accepting suggestions for alternate notations and systems.
Now that quantifiers are in both the I/O routines and in substitution, there need to be rules that use quantifiers. User interface issues are the main problem.
I need to rewrite the initialization code so that systems can be put together by gathering menu choices instead of requiring that the entire system be read in at once. That would allow having alternate PC basies for each modal logic system.
The parse trees that are drawn by the debugging code need to be made availiable as an output alternative. They are much too well liked.
I need to write an I/O module that understands dots (as Russell and Whitehead used) as in a>.b>c=..a>b>c.
One really ought to be able to change output notation in the middle of a proof. (So, for example, you can convert to a "pretty printed output" notation for printing without having to deal with it for the proof.)
The "Known Theorem" tables need to have some substatial lists added, instead of the current stubby 4.
When the proof is done, I need to have some cleanup commands.
The canned proof tables need some useful examples.
Much of the code needs to be split out as separate modules so that the other tools can make use of it.
Assumption and discharge display code needs to be added. (Argh... yet more work on the restrictions of the substition code.)
Should the internal form of the derivation be made availiable (I.E. should you be able to import and export them?)? They look roughly like: Example Derivation But the format is prone to change.
Should Substitution be a simple button, with the substitutions boxes themselves only displayed when you say you want to do one? It would make the output look dramaticly cleaner, but would mean it takes two screens to do a substitution.
Should axioms be dragged into the proof only as needed? (I think that they still need to be fully listed, but the proofs are shorter if only the axioms used appear in the final proof.)
How formal should combining systems be?
This page is http://www.cc.utah.edu/~nahaj/logic/calculate/ © Copyright 2001 by John Halleck, All Rights Reserved. This page was last modified on April 16th, 2001