9781568811451

Symbolic Computation and Automated Reasoning: The Calculemus-2000 Symposium

by
  • ISBN13:

    9781568811451

  • ISBN10:

    1568811454

  • Edition: 1st
  • Format: Hardcover
  • Copyright: 2001-04-02
  • Publisher: A. K. Peters

Note: Supplemental materials are not guaranteed with Rental or Used book purchases.

Purchase Benefits

  • Free Shipping On Orders Over $35!
    Your order must be $35 or more to qualify for free economy shipping. Bulk sales, PO's, Marketplace items, eBooks and apparel do not qualify for this offer.
  • Get Rewarded for Ordering Your Textbooks! Enroll Now
List Price: $89.95 Save up to $8.99
  • Rent Book $80.96
    Add to Cart Free Shipping

    TERM
    PRICE
    DUE

Supplemental Materials

What is included with this book?

  • The New copy of this book will include any supplemental materials advertised. Please check the title of the book to determine if it should include any access cards, study guides, lab manuals, CDs, etc.
  • The Rental copy of this book is not guaranteed to include any supplemental materials. Typically, only the book itself is included. This is true even if the title states it includes any access cards, study guides, lab manuals, CDs, etc.

Summary

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.

Table of Contents

PART I Regular Contributions 1(221)
Definite Integration of Parametric Rational Functions
3(15)
Andrew A. Adams
How to Find Symmetries Hidden in Combinatorial Problems
18(15)
Noriko H. Arai
Ryuji Masukawa
Communication Protocols for Mathematical Services
33(16)
Alessandro Armando
Michael Kohlhase
Silvio Ranise
Interfacing Computer Algebra and Deduction Systems
49(16)
Alessandro Armando
Daniele Zini
Development of the Theory of Continuous Lattices in Mizar
65(16)
Grzegorz Bancerek
Ω-Ants-Combining Interactive and Automated Theorem Proving
81(17)
Christoph Benzmuller
Volker Sorge
The THEOREMA Project: A Progress Report
98(16)
Bruno Buchberger
Claudio Dupre
Tudor Jebelean
Franz Kriftner
Koji Nakagawa
Daniela Vasaru
Wolfgang Windsteiger
How to Formally and Efficiently Prove Prime(2999)
114(12)
Olga Caprotti
Martijn Oostdijk
On the EA-Style Integrated Processing of Self-Contained Mathematical Texts
126(16)
Anatoli I. Degtyarev
Alexander V. Lyaletski
Marina K. Morokhovets
Towards Learning New Methods in Proof Planning
142(17)
Mateja Jamnik
Manfred Kerber
Christoph Benzmuller
Using Meta-variables for Natural Deduction in Theorema
159(16)
Boris Konev
Tudor Jebelean
Exploring Properties of Residue Classes
175(16)
Andreas Meier
Volker Sorge
Defining Power Series and Polynomials in Mizar
191(14)
Piotr Rudnicki
Christoph Schwarzweller
Andrzej Trybulec
Logic and Dependent Types in the Aldor Computer Algebra System
205(16)
Simon Thompson
PART II Invited Presentations 221(4)
Communicating Mathematics on the Web
223(1)
Henk Barendregt
Arjeh Cohen
Teaching Mathematics Accross the Internet
224(1)
Gaston H. Gonnet
PART III System Description 225(10)
Singular - A Computer Algebra System for Polynomial Computations
227(8)
Gert-Martin Greuel
Gerhard Pfister
Hans Schonemann
PART IV Posters 235(26)
Integration of Automated Reasoners: a Progress Report
237(2)
Alessandro Armando
Silvio Ranise
Daniele Zini
Algorithmic Theories and Context
239(2)
Clemens Ballarin
Jacques Calmet
The GiNaC Framework for Symbolic Computation...
241(2)
Christian Bauer
Alexander Frink
Richard Kreckel
A Framework for Propositional Model Elimination Algorithms
243(2)
Marco Benedetti
Resource Guided Concurrent Deduction
245(2)
Christoph Benzmuller
Mateja Jamnik
Manfred Kerber
Volker Sorge
Automated `Plugging and Chugging'
247(2)
Simon Colton
Integrating SAT solvers with domain-specific reasoners
249(2)
Fausto Giunchiglia
Roberto Sebastiani
Paolo Traverso
Solving Integrals at the Method Level
251(2)
Alex Heneveld
Ewen Maclean
Alan Bundy
Jacques Fleuriot
Alan Smaill
Lightweight Probability Theory for Verification
253(2)
Joe Hurd
St Andrews CAAR Group: Poster Abstract
255(2)
Tom Kelsey
OpenXM --- an Open System to Integrate Mathematical Software
257(2)
Masahide Maekawa
Yukio Okutani
Nobuki Takayama
Yasushi Tamura
Masayuki Noro
Katsuyoshi Ohara
Presentation of the Foc project
259(2)
Renaud Rioboo
Author Index 261(1)
Authors' Affiliations 261

Rewards Program

Write a Review