Mechanizing Mathematical Reasoning 机械化数学推理

By presenting state-of-the-art results in logical reasoning and formal methods in the context of artificial intelligence and AI applications, this book commemorates the 60th birthday of Jörg H. Siekmann.
The 30 revised reviewed papers are written by former and current students and colleagues of Jörg Siekmann; also included is an appraisal of the scientific career of Jörg Siekmann entitled "A Portrait of a Scientist: Logics, AI, and Politics." The papers are organized in four parts on logic and deduction, applications of logic, formal methods and security, and agents and planning.

A Portrait of a Scientist: Logic, AI and Politics
Logic and Deduction
Some Reflections on Proof Transformations
Rewrite and Decision Procedure Laboratory: Combining Rewriting,Satisfiability Checking, and Lemma Speculation
SAT-Based Decision Procedures for Automated Reasoning:A Unifying Perspective
Temporal Dynamics of Support and Attack Networks:From Argumentation to Zoology
Footprints of Conditionals
Time for Thinking Big in AI
Solving First-Order Constraints over the Monadic Class
From MKRP to ΩMEGA
　Decidable Variants of Higher-Order Unification
Normal Natural Deduction Proofs (in Non-classical Logics)
History and Future of Implicit and Inductionless Induction: Beware the Old Jade and the Zombie!
The Flowering of Automated Reasoning
Applications of Logics
Description Logics as Ontology Languages for the Semantic Web
Living Books, Automated Deduction and Other Strange Things
An Essay on Sabotage and Obstruction
Bridging Theorem Proving and Mathematical Knowledge Retrieval
Formal Description of Natural Languages:An HPSG Grammar of Polish
Psychological Validity of Schematic Proofs
Natural Language Proof Explanation
Why Proof Planning for Maths Education and How?
Formal Methods and Security
Towards MultiMedia Instruction in Safe and Secure Systems
The Impact of Models in Software Development
Formal Software Development in MAYA
A Unification Algorithm for Analysis of Protocols with Blinded Signatures
Exploiting Generic Aspects of Security Models in Formal Developments
Verification Support Environment
Agents and Planning
Author Index