No label defined (Q5287513)

The articles of this volume will not be indexed individually. The book is a carefully written and self-contained introduction to the HOL system, an interactive theorem-proving system for classical higher order logic. The HOL system is used for directly proving theorems and to support application-specific verification systems. The book contains a tutorial introduction and the basic material that is needed to work with the system. Part I contains a brief overview of HOL and describes the main ideas of the system. In Part II a detailed description of the ML language is presented. The programming language ML is provided by HOL. Part III contains a description of the logic which is supported by HOL. In its first chapter the syntax and semantics of the HOL logic is presented, the second chapter is devoted to the concept of a theory. Part IV describes how the HOL logic is embedded in ML. In particular, the ML functions representing the primitive inference rules are expounded. Part V presents the theorem-proving concepts that are provided by HOL. These include conversions, tacticals, tactics and derived inference rules. In summary, the book is of particular interest to people working in the areas of automated theorem proving and application-oriented verification systems.