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

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.

Perspicuity is part of proof. If the process by means of which I get a result were not surveyable, I might indeed make a note that this number is what comes out - but what fact is this supposed to confirm for me? I don't know 'what is supposed to come out' . . . . 1 -L. Wittgenstein A feasible computation uses small resources on an abstract computa- tion device, such as a 'lUring machine or boolean circuit. Feasible math- ematics concerns the study of feasible computations, using combinatorics and logic, as well as the study of feasibly presented mathematical structures such as groups, algebras, and so on. This volume contains contributions to feasible mathematics in three areas: computational complexity theory, proof theory and algebra, with substantial overlap between different fields. In computational complexity theory, the polynomial time hierarchy is characterized without the introduction of runtime bounds by the closure of certain initial functions under safe composition, predicative recursion on notation, and unbounded minimization (S. Bellantoni); 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. Downey and M. Fellows); new characterizations of PTIME and LINEAR SPACE are given using predicative recurrence over all finite tiers of certain stratified free algebras (D.

The theory of finite automata on finite stings, infinite strings, and trees has had a dis- tinguished history. First, automata were introduced to represent idealized switching circuits augmented by unit delays. This was the period of Shannon, McCullouch and Pitts, and Howard Aiken, ending about 1950. Then in the 1950s there was the work of Kleene on representable events, of Myhill and Nerode on finite coset congruence relations on strings, of Rabin and Scott on power set automata. In the 1960s, there was the work of Btichi on automata on infinite strings and the second order theory of one successor, then Rabin's 1968 result on automata on infinite trees and the second order theory of two successors. The latter was a mystery until the introduction of forgetful determinacy games by Gurevich and Harrington in 1982. Each of these developments has successful and prospective applications in computer science. They should all be part of every computer scientist's toolbox. Suppose that we take a computer scientist's point of view. One can think of finite automata as the mathematical representation of programs that run us- ing fixed finite resources. Then Btichi's SIS can be thought of as a theory of programs which run forever (like operating systems or banking systems) and are deterministic. Finally, Rabin's S2S is a theory of programs which run forever and are nondeterministic. Indeed many questions of verification can be decided in the decidable theories of these automata.

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 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.

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

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.

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.

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.

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.

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.

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 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.

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.

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 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.

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.

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.

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.

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.

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.