Symbolic Computation and Automated Reasoning
The CALCULEMUS-2000 Symposium
1st Edition
Published on 2. April 2001
Book
Hardback
284 pages
978-1-56881-145-1 (ISBN)
Description
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. This volume is devoted to the integration of computer algebra systems and deduction systems and the results presented will improve the automated design of hardware and software systems. The articles in this collection, presented at the 8th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, held August 6--7 in St. Andrews, Scotland, address all aspects relating deduction and computer algebra systems.
More details
Language
English
Place of publication
Natick
United States
Publishing group
Taylor & Francis Inc
Target group
College/higher education
Professional and scholarly
Dimensions
Height: 229 mm
Width: 152 mm
Weight
566 gr
ISBN-13
978-1-56881-145-1 (9781568811451)
Copyright in bibliographic data and cover images is held by Nielsen Book Services Limited or by the publishers or by their respective licensors: all rights reserved.
Schweitzer Classification
Other editions
Additional editions
Manfred Kerber | Michael Kohlhase
Symbolic Computation and Automated Reasoning
The CALCULEMUS-2000 Symposium
E-Book
04/2001
1st Edition
CRC Press
€73.49
Available for download
Manfred Kerber | Michael Kohlhase
Symbolic Computation and Automated Reasoning
The CALCULEMUS-2000 Symposium
E-Book
04/2001
CRC Press
€73.99
Available for download
Persons
Manfred Kerber, Michael Kohlhase
Content
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