Logic programming was based on first-order logic. Higher-order logics can also lead to theories of theorem-proving. This book introduces just such a theory, based on a lambda-calculus formulation of a clausal logic wi...
ISBN:
(纸本)9780521117906
Logic programming was based on first-order logic. Higher-order logics can also lead to theories of theorem-proving. This book introduces just such a theory, based on a lambda-calculus formulation of a clausal logic with equality, known as the Clausal Theory of Types. By restricting this logic to Horn clauses, a concise form of logic programming that incorporates functional programming is achieved. The book begins by reviewing the fundamental Skolem-Herbrand-Gödel Theorem and resolution, which are then extrapolated to a higher-order setting; this requires introducing higher-order equational unification which builds in higher-order equational theories and uses higher-order rewriting. The logic programming language derived has the unique property of being sound and complete with respect to Henkin-Andrews general models, and consequently of treating equivalent terms as identical. First published in 1993, the book can be used for graduate courses in theorem-proving, but will be of interest to all working in declarative programming.
Structured methodologies are a popular and powerful tool in information systems development. Many different ones exist, each employing a number of models and so a specification must be converted from one form to anoth...
详细信息
Structured methodologies are a popular and powerful tool in information systems development. Many different ones exist, each employing a number of models and so a specification must be converted from one form to another during the development process. To solve this problem, Dr. Tse proposes a unifying framework behind popular structured models. He approaches the problem from the viewpoints of algebra and category theory. He not only develops the frameworks but also illustrates their practical and theoretical usefulness. Thus, this book will provide insight for software engineers into how methodologies can be formalized, and will open up a range of applications and problems for theoreticalcomputer scientists.
The logic and methodology of design is examined in this book from the perspective of computerscience. computers provide the context for this examination both by discussion of the design process for hardware and softw...
详细信息
ISBN:
(纸本)9780521118156
The logic and methodology of design is examined in this book from the perspective of computerscience. computers provide the context for this examination both by discussion of the design process for hardware and software systems and by consideration of the role of computers in design in general. The central question posed by the author is whether or not we can construct a theory of design. This book concentrates upon the relationship between design, mathematics and science and thus its audience must include designers and software designers as well as computer scientists.
Originally published in 1988, this book presents an introduction to lambda-calculus and combinators without getting lost in the details of mathematical aspects of their theory. Lambda-calculus is treated here as a fun...
ISBN:
(纸本)9780521114295
Originally published in 1988, this book presents an introduction to lambda-calculus and combinators without getting lost in the details of mathematical aspects of their theory. Lambda-calculus is treated here as a functional language and its relevance to computerscience is clearly demonstrated. The main purpose of the book is to provide computerscience students and researchers with a firm background in lambda-calculus and combinators and show the applicabillity of these theories to functional programming. The presentation of the material is self-contained. It can be used as a primary text for a course on functional programming. It can also be used as a supplementary text for courses on the structure and implementation of programming languages, theory of computing, or semantics of programming languages.
This book describes the mathematical aspects of the semantics of programming languages. The main goals are to provide formal tools to assess the meaning of programming constructs in both a language-independent and a m...
ISBN:
(纸本)9780521062923
This book describes the mathematical aspects of the semantics of programming languages. The main goals are to provide formal tools to assess the meaning of programming constructs in both a language-independent and a machine-independent way, and to prove properties about programs, such as whether they terminate, or whether their result is a solution of the problem they are supposed to solve. In order to achieve this the authors first present, in an elementary and unified way, the theory of certain topological spaces that have proved of use in the modelling of various families of typed lambda calculi considered as core programming languages and as meta-languages for denotational semantics. This theory is known as Domain Theory, and was founded as a subject by Scott and Plotkin. One of the main concerns is to establish links between mathematical structures and more syntactic approaches to semantics, often referred to as operational semantics, which is also described. This dual approach has the double advantage of motivating computer scientists to do some mathematics and of interesting mathematicians in unfamiliar application areas from computerscience.
The goal of this book is to provide a comprehensive and systematic introduction to the important and highly applicable method of data refinement and the simulation methods used for proving its correctness. The authors...
详细信息
The goal of this book is to provide a comprehensive and systematic introduction to the important and highly applicable method of data refinement and the simulation methods used for proving its correctness. The authors concentrate in the first part on the general principles needed to prove data refinement correct. They begin with an explanation of the fundamental notions, showing that data refinement proofs reduce to proving simulation. The topics of Hoare Logic and the Refinement Calculus are introduced and a general theory of simulations is developed and related to them. Accessibility and comprehension are emphasized in order to guide newcomers to the area. The book's second part contains a detailed survey of important methods in this field, such as VDM, and the methods due to Abadi & Lamport, Hehner, Lynch and Reynolds, Back's refinement calculus and Z. All these methods are carefully analysed, and shown to be either imcomplete, with counterexamples to their application, or to be always applicable whenever data refinement holds. This is shown by proving, for the first time, that all these methods can be described and analyzed in terms of two simple notions: forward and backward simulation. The book is self-contained, going from advanced undergraduate level and taking the reader to the state of the art in methods for proving simulation.
Domain theory is an established part of theoreticalcomputerscience, used in giving semantics to programming languages and logics. In mathematics and logic it has also proved to be useful in the study of algorithms. ...
ISBN:
(纸本)9780521064798
Domain theory is an established part of theoreticalcomputerscience, used in giving semantics to programming languages and logics. In mathematics and logic it has also proved to be useful in the study of algorithms. This book is devoted to providing a unified and self-contained treatment of the subject. The theory is presented in a mathematically precise manner which nevertheless is accessible to mathematicians and computer scientists alike. The authors begin with the basic theory including domain equations, various domain representations and universal domains. They then proceed to more specialized topics such as effective and power domains, models of lambda-calculus and so on. In particular, the connections with ultrametric spaces and the Kleene–Kreisel continuous functionals are made precise. Consequently the text will be useful as an introductory textbook (earlier versions have been class-tested in Uppsala, Gothenburg, Passau, Munich and Swansea), or as a general reference for professionals in computerscience and logic.
Declarative programs consist of mathematical functions and relations and are amenable to formal specification and verification, since the methods of logic and proof can be applied to the programs in a well-defined man...
详细信息
ISBN:
(数字)9780511880704
ISBN:
(纸本)9780521032513
Declarative programs consist of mathematical functions and relations and are amenable to formal specification and verification, since the methods of logic and proof can be applied to the programs in a well-defined manner. Here Dr Padawitz emphasizes verification based on logical inference rules, i.e. deduction (in contrast with model-theoretic approaches, deductive methods can be automated to some extent). His treatment of the subject differs from others in that he tries to capture the actual styles and applications of programming; neither too general with respect to the underlying logic, nor too restrictive for the practice of programming. He generalizes and unifies results from classical theorem-proving and term rewriting to provide proof methods tailored to declarative program synthesis and verification. Detailed examples accompany the development of the methods, whose use is supported by a documented prototyping system. The book can be used for graduate courses or as a reference for researchers in formal methods, theorem-proving and declarative languages.
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.
暂无评论