This is a comprehensive introduction to many-sorted logic - a variety of classical logic with applications to computer science, artificial intelligence and mathematics. Computer science is essentially many-sorted; its reasoning is based on composite structures, such as elements and functions, data and programmes, data and time. Following a detailed introduction to the theory of many-sorted first-order logic as a universal logic encompassing a range of other logical systems, the book then focuses on its important application areas within computer science research. It requires only a basic knowledge of mathematical logic and will be of value to computer scientists, mathematicians and philosophers.
ALGEBRAIC METHODS; Equational Specifications for Computable Data Types: Six Hidden Functions Suffice and Other Sufficiency Bounds (J. Bergstra & J. Tucker); On Bounds for the Specification of Finite Data Types by Means of Equations and Conditional Equations (J. Bergstra & J. Tucker); Many-Sorted Logics and Algebraic Semantics (I. Guessarian); Subdirect Representation of Higher-Order Algebras (K. Meinke); FOUNDATIONS OF ARTIFICIAL INTELLIGENCE; On the Appearance of Sortal Literals: A Non-Substitutional Approach to Hybrid Reasoning (A. Cohn); An Order-Sorted Predicate Logic with Closely Coupled Taxonomic Information (C. Beierle, et al.); FOUNDATIONS OF PROGRAM VERIFICATION; Comparing and Characterizing the Powers of Established Program Verification Methods (I. Sain); An Infinite Hierarchy of Program Verification Methods (A. Pasztor); Standard Versus Non-Standard Semantics in Logics for Functional Programs (A. Gil-Luezas, et al.); Index.