Wish list/suggested enhancements/silly ideas, from the point of view
of someone who has just started using DC Proof

1) Hot Keys for the most common functions, such as the application of
Modus Ponens/Detachment

2) Picklist of possible transformations - the user jumps into some
kind of SUGGEST TRANSFORMATIONS mode, and clicks on any number of
statements. The user is then presented with a picklist of relevant
rules which could be applied to the given set of statements.

3) Ability to group sets of .Proof files, extract their conclusions
(with/without associated comments), and join them all into a set of
axioms, which are then auto-pasted to the top of the current file.

4) String substitution in the conclusion - like substituting 'Socrates
is mortal' for 'M(s)', or 'Politicians lie' for 'L(p)' at the end of
the proof.


4a) Alternative to 4) - A separate definition file for any given
proof, specifying the initial string substitutions mentioned in (4)
above, and a separate conclusion file, which takes the conclusion at
the end of the current .PROOF file, performs the string substitutions,
and outputs the desired strings into the separate conclusion file.


5 Command line capability - something like

DCPROOFCMD.EXE <FileName>.PROOF ADDPREMISE "(A=>B)=>C"
DCPROOFCMD.EXE <FileName>.PROOF ADDPREMISE "(A=>B)"
DCPROOFCMD.EXE <FileName>.PROOF DETACH "1,2" (Not sure how you would
obtain the line numbers 1 and 2, but that's the general idea)

5a) Some means of returning various result values, e.g. line numbers,
from each command line referenced in 5. The idea would be that batch
files could be used as a script language for DCPROOF.


6) A Pocket PC or Texas Instruments (e.g. TI-92 or Voyage 200) version