This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application,...
详细信息
ISBN:
(数字)9781316044537
ISBN:
(纸本)9780521779111
This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply them elsewhere in much more complex settings. There are numerous exercises throughout the text. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoreticalcomputerscience and artificial intelligence. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included.
All traditional implementation techniques for functional languages (mostly based on supercombinators, environments or continuations) fail to avoid useless repetition of work; they are not 'optimal' in their im...
ISBN:
(纸本)9780521621120
All traditional implementation techniques for functional languages (mostly based on supercombinators, environments or continuations) fail to avoid useless repetition of work; they are not 'optimal' in their implementation of sharing, often causing a catastrophic, exponential explosion in reduction time. Optimal reduction is an innovative graph reduction technique for functional expressions, introduced by Lamping in 1990, that solves the sharing problem. This book, the first in the subject, is a comprehensive account by two of its leading exponents. Practical implementation aspects are fully covered as are the mathematical underpinnings of the subject. The relationship to the pioneering work of Levy and to Girard's more recent Geometry of Interaction are explored; optimal reduction is thereby revealed as a prime example of how a beautiful mathematical theory can lead to practical benefit. The book is essentially self-contained, requiring no more than basic familiarity with functional languages. It will be welcomed by graduate students and research workers in lambda calculus, functional programming or linear logic.
Mathematicians from Leibniz to Hilbert have sought to mechanise the verification of mathematical proofs. Developments arising out of Gödel's proof of his incompleteness theorem showed that no computer program...
详细信息
ISBN:
(数字)9780511881381
ISBN:
(纸本)9780521585330
Mathematicians from Leibniz to Hilbert have sought to mechanise the verification of mathematical proofs. Developments arising out of Gödel's proof of his incompleteness theorem showed that no computer program could automatically prove true all the theorems of mathematics. In practice, however, there are a number of sophisticated automated reasoning programs that are quite effective at checking mathematical proofs. Now in paperback, this book describes the use of a computer program to check the proofs of several celebrated theorems in metamathematics including Gödel's incompleteness theorem and the Church–Rosser theorem. The computer verification using the Boyer–Moore theorem prover yields precise and rigorous proofs of these difficult theorems. It also demonstrates the range and power of automated proof checking technology. The mechanisation of metamathematics itself has important implications for automated reasoning since metatheorems can be applied by labour-saving devices to simplify proof construction. The book should be accessible to scientists and philosophers with some knowledge of logic and computing.
Type theory is one of the most important tools in the design of higher-level programming languages, such as ML. This book introduces and teaches its techniques by focusing on one particularly neat system and studying ...
详细信息
ISBN:
(数字)9780511834738
ISBN:
(纸本)9780521054225
Type theory is one of the most important tools in the design of higher-level programming languages, such as ML. This book introduces and teaches its techniques by focusing on one particularly neat system and studying it in detail. In this way, all the key ideas are covered without getting involved in the complications of more advanced systems, but concentrating rather on the principles that make the theory work in practice. This book takes a type-assignment approach to type theory, and the system considered is the simplest polymorphic one. The author covers all the basic ideas, including the system's relation to propositional logic, and gives a careful treatment of the type-checking algorithm which lies at the heart of every such system. Also featured are two other interesting algorithms that have been buried in inaccessible technical literature. The mathematical presentation is rigorous but clear, making the book at a level which can be used as an introduction to type theory for computer scientists.
Petri nets are a popular and powerful formal model for the analysis and modelling of concurrent systems, and a rich theory has developed around them. Petri nets are taught to undergraduates, and also used by industria...
详细信息
ISBN:
(数字)9780511885822
ISBN:
(纸本)9780521019453
Petri nets are a popular and powerful formal model for the analysis and modelling of concurrent systems, and a rich theory has developed around them. Petri nets are taught to undergraduates, and also used by industrial practitioners. This book focuses on a particular class of petri nets, free choice petri nets, which play a central role in the theory. The text is very clearly organised, with every notion carefully explained and every result proved. Clear exposition is given for place invariants, siphons, traps and many other important analysis techniques. The material is organised along the lines of a course book, and each chapter contains numerous exercises, making this book ideal for graduate students and research workers alike.
From the Publisher: Epistemic logic has grown from its philosophical beginnings to find diverse applications in computerscience as a means of reasoning about the knowledge and belief of agents. This book, based on co...
详细信息
ISBN:
(纸本)052146014X;1141331411
From the Publisher: Epistemic logic has grown from its philosophical beginnings to find diverse applications in computerscience as a means of reasoning about the knowledge and belief of agents. This book, based on courses taught at universities and summer schools, provides a broad introduction to the subject; many exercises are included as well as their solutions. After presenting the necessary apparatus from mathematics and logic, the authors consider applications in the areas of common knowledge, distributed knowledge, explicit and implicit belief.
暂无评论