Bøger i Progress in Computer Science and Applied Logic serien

The natural measure of difficulty of a function is the amount of time needed to compute it (as a function of the length of the input). In recursion theory, by contrast, a function is considered to be easy to compute if there exists some algorithm that computes it.

A so-called "effective" algorithm may require arbitrarily large finite amounts of time and space resources, and hence may not be practical in the real world. A "feasible" algorithm is one which only requires a limited amount of space and/or time for execution; the general idea is that a feasible algorithm is one which may be practical on today's or at least tomorrow's computers. There is no definitive analogue of Church's thesis giving a mathematical definition of feasibility; however, the most widely studied mathematical model of feasible computability is polynomial-time computability. Feasible Mathematics includes both the study of feasible computation from a mathematical and logical point of view and the reworking of traditional mathematics from the point of view of feasible computation. The diversity of Feasible Mathematics is illustrated by the. contents of this volume which includes papers on weak fragments of arithmetic, on higher type functionals, on bounded linear logic, on sub recursive definitions of complexity classes, on finite model theory, on models of feasible computation for real numbers, on vector spaces and on recursion theory. The vVorkshop on Feasible Mathematics was sponsored by the Mathematical Sciences Institute and was held at Cornell University, June 26-28, 1989.

This book brings together contributions by leading researchers in computational complexity theory written in honor of Somenath Biswas on the occasion of his sixtieth birthday.

The aim of this volume is to collect original contributions by the best specialists from the area of proof theory, constructivity, and computation and discuss recent trends and results in these areas.

an alternative way of looking at NP problems is introduced which focuses on which pa rameters of the problem are the cause of its computational complexity and completeness, density and separation/collapse results are given for a struc ture theory for parametrized problems (R.

The field of computational learning theory arose out of the desire to for mally understand the process of learning. Scholars in both fields came together to learn about each others' field and to look for common ground, with the ultimate goal of providing a new model of learning from geometrical examples that would be useful in computer vision.

This book brings together contributions by leading researchers in computational complexity theory written in honor of Somenath Biswas on the occasion of his sixtieth birthday.

The twenty-six papers in this volume reflect the wide and still expanding range of Anil Nerode's work. Recursive model theory is the subject of papers by Hird, Moses, and Khoussainov & Dadajanov, while a combinatorial problem in recursive model theory is discussed in Cherlin & Martin's paper.

The natural measure of difficulty of a function is the amount of time needed to compute it (as a function of the length of the input). In recursion theory, by contrast, a function is considered to be easy to compute if there exists some algorithm that computes it.

A large part of the monograph is devoted to detailed proofs that the methods we present are sound and complete, which in the context of the logic programming, means that the operational and denotational semantics agree.

FunctionQl areas which are, or are becoming, sources of exciting problems are computer performance analysis, data base analysis, analysis of communication protocols, data networks, and mixed voice-data telephone networks.

A spline is a thin flexible strip composed of a material such as bamboo or steel that can be bent to pass through or near given points in the plane, or in 3-space in a smooth manner. The same mathematical ideas used for computing "spline" curves can be extended to allow us to compute "spline" surfaces.

In the research community the field of robotics has recently reached large size and respectability, but without answering the question, "What is robotics?" Rather than try to enumerate all of the things that are and are not robots, I will try to characterize the kinds of features that make a system a robot.

The field of computational learning theory arose out of the desire to for mally understand the process of learning. Scholars in both fields came together to learn about each others' field and to look for common ground, with the ultimate goal of providing a new model of learning from geometrical examples that would be useful in computer vision.

The twenty-six papers in this volume reflect the wide and still expanding range of Anil Nerode's work. Recursive model theory is the subject of papers by Hird, Moses, and Khoussainov & Dadajanov, while a combinatorial problem in recursive model theory is discussed in Cherlin & Martin's paper.

The book introduces new techniques which imply rigorous lower bounds on the complexity of some number theoretic and cryptographic problems. These functions are considered over the residue ring modulo p and over the residue ring modulo an arbitrary divisor d of p - 1.

FunctionQl areas which are, or are becoming, sources of exciting problems are computer performance analysis, data base analysis, analysis of communication protocols, data networks, and mixed voice-data telephone networks.

The conference was planned for June 2003 with the official title Workshop on Coding, Cryptography and Combi natorics (CCC 2003). Those who are familiar with events in East Asia in the first half of 2003 can guess what happened in the end, namely the conference had to be cancelled in the interest of the health of the participants.

The book introduces new techniques which imply rigorous lower bounds on the complexity of some number theoretic and cryptographic problems. These functions are considered over the residue ring modulo p and over the residue ring modulo an arbitrary divisor d of p - 1.

In this monograph we study two generalizations of standard unification, E-unification and higher-order unification, using an abstract approach orig inated by Herbrand and developed in the case of standard first-order unifi cation by Martelli and Montanari.

In the winter of 1978, Professor George P61ya and I jointly taught Stanford University's introductory combinatorics course. Enumerative combinatorics deals with the counting of combinatorial objects. Existential combinatorics studies the existence or nonexistence of combinatorial configurations.

Hashing algorithms scramble data and create pseudo-uniform data distribu­ tions. Bucket algorithms operate on raw untransformed data which are parti­ tioned Into groups according to membership In equl-slzed d-dlmenslonal hyperrec­ tangles, called cells or buckets. The bucket data structure Is rather sensitive to the distribution of the data. In these lecture notes, we attempt to explain the connection between the expected time of various bucket algorithms and the dis­ tribution of the data. The results are Illustrated on standard searching, sorting and selection problems, as well as on a variety of problems In computational geometry and operations research. The notes grew partially from a graduate course on probability theory In computer science. I wish to thank Elizabeth Van Gulick for her help with the manuscript, and David Avis, Hanna AYukawa, Vasek Chvatal, Beatrice Devroye, Hossam EI Glndy, Duncan McCallum, Magda McCallum, Godfrled Toussaint and Sue Whltesldes"for making the School of Computer Science at McGill University such an enjoyable place. The work was supported by NSERC Grant A3456 and by FCAC Grant EQ-1679. INTRODUCTION 1 INTRODUCTION It Is not a secret that methods based upon the truncation of data have good expected time performance. For example, for nice distributions of the data, searching Is often better done via a hashing data structure Instead of via a search tree. The speed one observes In practice Is due to the fact that the truncation operation Is a constant time operation.

The synthesis rules may be used when a program is first being developed, or when, in the course of modifying a program, the need arises to rewrite a program segment.

This innovative monograph explores a new mathematical formalism in higher-order temporal logic for proving properties about the behavior of systems.

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 Gröbner 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 Techniques workshop, which was held at the Centro Stefano Franscini in Ascona, Switzerland, from April 30 to May 4, 1995. That workshop brought together 40 researchers from various areas of rewriting techniques, the main goal being the investigation of common threads and methods. Following the workshops, each contribution was formally refereed and 14 papers were selected for publication.

This volume contains the refereed proceedings of the Workshop on Cryptography and Computational Number Theory, CCNT'99, which has been held in Singapore during the week of November 22-26, 1999. The idea for this workshop grew out of the recognition of the recent, rapid development in various areas of cryptography and computational number the ory.

The book introduces new techniques that imply rigorous lower bounds on the com plexity of some number-theoretic and cryptographic problems. These functions are considered over the residue ring modulo p and over the residue ring modulo an arbitrary divisor d of p - 1.

Mathematical logic is a branch of mathematics that takes axiom systems and mathematical proofs as its objects of study. This book shows how it can also provide a foundation for the development of information science and technology. The first five chapters systematically present the core topics of classical mathematical logic, including the syntax and models of first-order languages, formal inference systems, computability and representability, and Godel's theorems. The last five chapters present extensions and developments of classical mathematical logic, particularly the concepts of version sequences of formal theories and their limits, the system of revision calculus, proschemes (formal descriptions of proof methods and strategies) and their properties, and the theory of inductive inference. All of these themes contribute to a formal theory of axiomatization and its application to the process of developing information technology and scientific theories. The book also describes the paradigm of three kinds of language environments for theories and it presents the basic properties required of a meta-language environment. Finally, the book brings these themes together by describing a workflow for scientific research in the information era in which formal methods, interactive software and human invention are all used to their advantage.The second edition of the book includes major revisions on the proof of the completeness theorem of the Gentzen system and new contents on the logic of scientific discovery, R-calculus without cut, and the operational semantics of program debugging.This book represents a valuable reference for graduate and undergraduate students and researchers in mathematics, information science and technology, and other relevant areas of natural sciences. Its first five chapters serve as an undergraduate text in mathematical logic and the last five chapters are addressed to graduate students in relevant disciplines.

The conference was planned for June 2003 with the official title Workshop on Coding, Cryptography and Combi natorics (CCC 2003). Those who are familiar with events in East Asia in the first half of 2003 can guess what happened in the end, namely the conference had to be cancelled in the interest of the health of the participants.