Hi,

Thanks for the suggestions. Below, you will find some suggestions to help
you achieve at least some of the functionality you are looking for, using
the current version.

----- Original Message -----
From: "iquine" <iquine@...>
To: <dcproof@yahoogroups.com>
Sent: Wednesday, June 08, 2005 8:59 AM
Subject: [DC Proof] Wish list/suggested enhancement/silly ideas


> 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
>

See the tool bar. The 'Det' button invokes Detachment, the 'U Gen' button
invokes Universal Generalization, etc.


> 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.
>

The number of possibilities are limitless. I wouldn't know where to begin!

The colour and font of the variables, however, do suggest some possibilites.
Or at least eliminate some. The colour of the variables indicate what kind
of generalizations are possible -- green for universal, and red for
existential generalizations. A variable in a bold font rules out an
immediate conclusion.


> 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.
>

You can copy the text of a conclusion or generalization from one proof into
the premise of another. See 'Edit Menu Options.' You can have several
occurrences of DC Proof open at once, a different proof displayed in each
one.


> 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.
>

You can use any number of characters to make meaningful names for
predicates, propositions and variables. You could, to use your example,
have:

1 ALL(x):[Man(x) => Mortal(x)]
Premise

2 Man(socrates)
Premise

3 Man(socrates) => Mortal(socrates)
U Spec, 1

4 Mortal(socrates)
Detach, 3, 2


>
> 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.
>

See reply to number 3. If you copy in a generalization, you can apply it to
any free variables in another proof.


>
> 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.
>

Sorry, I don't see any advantage in this. It would be like playing chess in
your head! Wouldn't you really rather use a nice graphical interface?


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

Don't they have rather small screens, and no colour? For these reasons, I
think they would be rather awkward to use for an application like DC Proof.
At times, you really do need to see the "big picture" -- the bigger the
better. At times, you may even want to use the smallest font to view as many
lines at once as possible.

Dan