Description: One Interactive Theorem Proving.- 1. Structured Specifications and Interactive Proofs with KIV.- 2. Proof Theory at Work: Program Development in the Minlog System.- 3. Interactive and automated proof construction in type theory.- 4. Integrating Automated and Interactive Theorem Proving.- Two Representation and Optimization Techniques.- 5. Term Indexing.- 6. Developing Deduction Systems: The Toolbox Style.- 7. Specifications of Inference Rules: Extensions of the PTTP Technique.- 8. Proof Analysis, Generalization and Reuse.- Three Parallel Inference Systems.- 9. Parallel Term Rewriting with PaReDuX.- 10. Parallel Theorem Provers Based on SETHEO.- 11. Massively Parallel Reasoning.- Four Comparision and Cooperation of Theorem Provers.- 12. Extension Methods in Automated Deduction.- 13. A Comparison of Equality Reasoning Heuristics.- 14. Cooperating Theorem Provers.

Please Wait