- automated adaptation of proof presentation to the knowledge of the reader (Inferences from well known theories such as pure logic are suppressed)
- interactive transformation of proofs to achieve better readability of proof presentation (e. g. conversion direct-indirect)
- automated combination of proofs from different sytems into more complex proofs and complete manuscripts including proofs of lemmata.
- automated verification of applicability of lemmata ("Obviously we did not use the commutativity of the group in the proof of Theorem ... Therefore we can apply this Theorem now." "This was proved by ... in a constructive manner")
2)
> However, if a single system captures the
> hearts and minds of mathematicians then the logic of that system could
> become a defacto standard and translation could become irrelevant. No
> matter how strong our cooperative tendencies are, I think that
> ultimately the nature of machine verification will be decided in a
> free market fasion with mathematicians playing the role of consumers.
> A single system will probably dominate.
If you ask a mathematician (not being a logician) which logical system dominates his thinking, he will - probably - not even understand the question! He "argues" in an informal manner, but being ready to formalize as far as to make sure the unambiguity of his argument. Therefore logic is usually explicit only in the first semester where the student has to learn how to understand the teacher (NB: As a math student I had to attend a lecture on differential equations where everything on the blackboard was formalized in manysorted first order logic - it was precise, but awful.)
The consequence I see for QED is: A QED-system aiming at mathematicians should hide the logic unless the user wants access to it. Therefore, there may be several QED-systems using different logics. Whether a system is accepted will be much more dependent on it's user interface, especially on it's ability to model the language normally used by mathematicians. But an important argument for a system will also be it's ability to import theorems and proofs from other systems or from a central book store.
3) Logical systems are concerned with proofs - not with truth ([almost] no automated theorem prover incorporated any idea of semantics). Therefore, only the syntactic approach makes sense to me.
Ingo Dahn