Rippling is a radically new technique for the automation of mathematical reasoning. It is widely applicable whenever a goal is to be proved from one or more syntactically similar givens. It was originally developed fo...
详细信息
ISBN:
(数字)9781316905692
ISBN:
(纸本)9780521834490
Rippling is a radically new technique for the automation of mathematical reasoning. It is widely applicable whenever a goal is to be proved from one or more syntactically similar givens. It was originally developed for inductive proofs, where the goal was the induction conclusion and the givens were the induction hypotheses. It has proved to be applicable to a much wider class of tasks, from summing series via analysis to general equational reasoning. The application to induction has especially important practical implications in the building of dependable IT systems, and provides solutions to issues such as the problem of combinatorial explosion. Rippling is the first of many new search control techniques based on formula annotation; some additional annotated reasoning techniques are also described here. This systematic and comprehensive introduction to rippling, and to the wider subject of automated inductive theorem proving, will be welcomed by researchers and graduate students alike.
This book discusses the connection between two areas of semantics, namely the semantics of databases and the semantics of natural language, and links them via a common view of the semantics of time. It is argued that ...
详细信息
ISBN:
(数字)9780511874345
ISBN:
(纸本)9780521602747
This book discusses the connection between two areas of semantics, namely the semantics of databases and the semantics of natural language, and links them via a common view of the semantics of time. It is argued that a coherent theory of the semantics of time is an essential ingredient for the success of efforts to incorporate more 'real world' semantics into database models. This idea is a relatively recent concern of database research but it is receiving growing interest. The book begins with a discussion of database querying which motivates the use of the paradigm of Montague Semantics and discusses the details of the intensional logic ILs. This is followed by a description of the author's own model, the Historical Relational Data Model (HRDM) which extends the RDM to include a temporal dimension. Finally the database querying language QEHIII is defined and examples illustrate its use. A formal model for the interpretation of questions is presented in this work which will form the basis for much further research.
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 univ...
ISBN:
(纸本)9780521602808
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 together with their solutions. The authors begin by presenting the necessary apparatus from mathematics and logic, including Kripke semantics and the well-known modal logics K, T, S4 and S5. Then they turn to applications in the contexts of distributed systems and artificial intelligence: topics that are addressed include the notions of common knowledge, distributed knowledge, explicit and implicit belief, the interplays between knowledge and time, and knowledge and action, as well as a graded (or numerical) variant of the epistemic operators. The problem of logical omniscience is also discussed extensively. Halpern and Moses' theory of honest formulae is covered, and a digression is made into the realm of non-monotonic reasoning and preferential entailment. Moore's autoepistemic logic is discussed, together with Levesque's related logic of 'all I know'. Furthermore, it is shown how one can base default and counterfactual reasoning on epistemic logic.
Belief revision is a topic of much interest in theoreticalcomputerscience and logic, and it forms a central problem in research into artificial intelligence. In simple terms: how do you update a database of knowledg...
详细信息
ISBN:
(数字)9780511879838
ISBN:
(纸本)9780521545648
Belief revision is a topic of much interest in theoreticalcomputerscience and logic, and it forms a central problem in research into artificial intelligence. In simple terms: how do you update a database of knowledge in the light of new information? What if the new information is in conflict with something that was previously held to be true? An intelligent system should be able to accommodate all such cases. This book contains a collection of research articles on belief revision that are completely up to date and an introductory chapter that presents a survey of current research in the area and the fundamentals of the theory. Thus this volume will be useful as a textbook on belief revision.
This book discusses recent research in the theoretical foundations of several subjects of importance for the design of hardware, and for computerscience in general. The physical technologies of very large scale integ...
ISBN:
(纸本)9780521545655
This book discusses recent research in the theoretical foundations of several subjects of importance for the design of hardware, and for computerscience in general. The physical technologies of very large scale integration (VLSI) are having major effects on the electronic industry. The potential diversity and complexity of digital systems have begun a revolution in the technologies of digital design, involving the application of concepts and methods to do with algorithms and programming. In return, the problems of VLSI design have led to new subjects becoming of importance in computerscience. Topics covered in this volume include: models of VLSI complexity; complexity theory; systolic algorithm design; specification theory; verification theory; design by stepwise refinement and transformations. A thorough literature survey with an exhaustive bibliography is also included. The book has grown from a workshop held at the Centre for theoreticalcomputerscience at Leeds University and organised by the editors.
This is a systematic and comprehensive introduction both to compositional proof methods for the state-based verification of concurrent programs, such as the assumption-commitment and rely-guarantee paradigms, and to n...
详细信息
ISBN:
(纸本)0521806089;9780521806084
This is a systematic and comprehensive introduction both to compositional proof methods for the state-based verification of concurrent programs, such as the assumption-commitment and rely-guarantee paradigms, and to noncompositional methods, whose presentation culminates in an exposition of the communication-closed-layers (CCL) paradigm for verifying network protocols.
暂无评论