Symbolic Computation and Automated Reasoning: The CALCULEMUS-2000 Symposium,9781568811451

Symbolic Computation and Automated Reasoning: The CALCULEMUS-2000 Symposium

by
Edition: 1st
ISBN13: 9781568811451
ISBN10: 1568811454
Format: Hardcover
Pub. Date: 2001-04-02
Publisher(s): A. K. Peters
List Price: $105.83

Buy New

Usually Ships in 5-7 Business Days
$100.79
Add to Cart

Rent Textbook

Select for Price
Add to Cart
There was a problem. Please try again later.

Rent Digital

Rent Digital Options
Online:180 Days access
Downloadable:180 Days
$48.84
Online:365 Days access
Downloadable:365 Days
$57.72
Online:1825 Days access
Downloadable:Lifetime Access
$88.79
*To support the delivery of the digital material to you, a non-refundable digital delivery fee of $3.99 will be charged on each digital item.
$48.84*
Add to Cart

Used Textbook

We're Sorry
Sold Out

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

An electronic version of this book is available through VitalSource.

This book is viewable on PC, Mac, iPhone, iPad, iPod Touch, and most smartphones.

By purchasing, you will be able to view this book online, as well as download it, for the chosen number of days.

Digital License

You are licensing a digital product for a set duration. Durations are set forth in the product description, with "Lifetime" typically meaning five (5) years of online access and permanent download to a supported device. All licenses are non-transferable.

More details can be found here.

A downloadable version of this book is available through the eCampus Reader or compatible Adobe readers.

Applications are available on iOS, Android, PC, Mac, and Windows Mobile platforms.

Please view the compatibility matrix prior to purchase.