A Nifty Tool: ProofBuilder, an Interactive Proof Assistant, with Extensive Capabilities

* work in progress

* proof assistant
re other proof assistants, people say: requires expertise
but students need to learn to construct proofs

* purpose: help student being formal, doing symbol manipulations
avoid mistakes e.g. setting up induction
but student still needs to think deductively (not automatic theorem prover)

* trying to be sufficient but not excessive, small not necessarily theoretically perfect

* standard symbols "≤", "∀", "∪", "∑", ...

* options for conforming to different preferences
e.g. implication "⇒" or "→"
e.g. conjunction "∧" or "AND"

* to handle formal aspects, using format two-column multi-row "deductive tableau" [Manna & Waldinger]
clarifying hypotheses, goal/subgoals that still need to prove

* extensive range of deductions / proof strategies
- induction (stepwise, well-founded)
- rewritings
- proof by contradiction
- proof by cases
- quantifier removal
- nonclausal resolution (covering modus ponens)
- substituting using equations
- substituting using equivalences
- transforming one side of equation/equivalence to the other

* future work
- provide options that even wider range of people may want
- improve interface
o enable more 'editing' of proof
o enable more proper exponents, summation limits
o built-in help facilities
- improve documentation
.
. see what's desired from more use
.