Symbolic Computation and Automated Reasoning de Manfred Kerber

Symbolic Computation and Automated Reasoning: The CALCULEMUS-2000 Symposium

Manfred Kerber

Michael Kohlhase

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.

Citește tot Restrânge

Cuprins

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