Symbolic Computation and Automated Reasoning: The CALCULEMUS-2000 Symposium

by Manfred Kerber (Editor), Michael Kohlhase (Editor)

Overview

While mathematical software packages are commercially successful and widely used, the use of formal methods in hardware and software development is also becoming more and more important and necessary. This has made deduction systems indispensable because of the complexity and sheer size of the reasoning tasks involved.

Product Details

ISBN-13:	9781040186848
Publisher:	CRC Press
Publication date:	04/02/2001
Sold by:	Barnes & Noble
Format:	eBook
Pages:	288
File size:	5 MB

About the Author

Manfred Kerber, Michael Kohlhase

Table of Contents

Part I: Regular Contributions; Definite Integration of Parametric Rational Functions: Applying a DITLU; How to Find Symmetries Hidden in Combinatorial Problems; Communication Protocols for Mathematical Services based on KQML and OMRS; Interfacing Computer Algebra and Deduction Systems via the Logic Broker Architecture; Development of the Theory of Continuous Lattices in MIZAR; ?-ANTS – An Open Approach at Combining Interactive and Automated Theorem Proving; The TH?OREM? Project: A Progress Report; How to Formally and Efficiently Prove Prime(2999); On the EA-Style Integrated Processing of Self-Contained Mathematical Texts; Towards Learning New Methods in Proof Planning; Using Meta-variables for Natural Deduction in Theorema; Exploring Properties of Residue Classes; Defining Power Series and Polynomials in Mizar; Logic and Dependent Types in the Aldor Computer Algebra System; Part II: Invited Presentations; Communicating Mathematics on the Web; Teaching Mathematics Accross the Internet; Part III: System Description; Singular — A Computer Algebra System for Polynomial Computations; Part IV: Posters; Integration of Automated Reasoners: a Progress Report; Algorithmic Theories and Context; The GiNaC Framework for Symbolic Computation within the C++ Programming Language; A Framework for Propositional Model Elimination Algorithms; Resource Guided Concurrent Deduction; Automated ‘Plugging and Chugging’; Integrating SAT Solvers with Domain-specific Reasoners; Solving Integrals at the Method Level; Lightweight Probability Theory for Verification; St Andrews CAAR Group: Poster Abstract; OpenXM — an Open System to Integrate Mathematical Software; Presentation of the Foc Project

Editorial Reviews

Computer scientists from Europe, Japan, and Canada explore the integration of existing deduction systems and computer algebra systems in light of the increasing complexity of software and hardware development, which makes the use of formal methods of mathematics more important. Two invited presentations discuss communicating mathematics across the Internet and Web. Among the other 27 topics are interfacing computer algebra and deduction systems, exploring properties of residue classes, algorithm theories and context, and lightweight probability theory for verification. There is no subject index. Annotation c. Book News, Inc., Portland, OR (booknews.com)

Booknews