Mechanizing Mathematical Reasoning 机械化数学推理

出版时间：2005-4  出版社：北京燕山出版社  作者：Hutter, Dieter; Stephan, Werner;  页数：563  
Tag标签：无  

内容概要

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 PoliticsLogic 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 ReasoningApplications 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 EnvironmentAgents and PlanningAuthor Index