ether (12/02/82)
I am looking for a 'logic blackboard' (for want of
a better name) which would be an interactive formula
manipulator. Mainly, this would
a) check a given step for agreement with the rule
which supposedly generated it (proof checker mode), and
b) perform certain error prone grunt work (like conversion
to conjunctive normal form, etc).
The idea is not to have a general (?) theorem prover, but
something which would decrease the frequency of dropped
terms and negation signs while working out ideas or trying
to prove things.
Does anyone have/know of such a wondrous system?