This monograph develops techniques for equational reasoning in higher-order logic. Due to its expressiveness, higher-order logic is used for specification and verification of hardware, software, and mathematics. In these applica tions, higher-order logic provides the necessary level of abstraction for con cise and natural formulations. The main assets of higher-order logic are quan tification over functions or predicates and its abstraction mechanism. These allow one to represent quantification in formulas and other variable-binding constructs. In this book, we focus on equational logic as a...

The fields of cryptography and computational number theory have recently witnessed a rapid development, which was the subject of the CCNT workshop in Singapore in November 1999. Its aim was to stimulate further research in information and computer security as well as the design and implementation of number theoretic cryptosystems and other related areas. Another achievement of the meeting was the collaboration of mathematicians, computer scientists, practical cryptographers and engineers in academia, industry and government. The present volume comprises a selection of refereed papers...

Symbolic rewriting techniques are methods for deriving consequences from systems of equations, and are of great use when investigating the structure of the solutions. Such techniques appear in many important areas of research within computer algebra: the Knuth-Bendix completion for groups, monoids and general term-rewriting systems; the Buchberger algorithm for Grobner bases; the Ritt-Wu characteristic set method for ordinary differential equations; and the Riquier-Janet method for partial differential equations. This volume contains invited and contributed papers to the "Symbolic Rewriting...