This is the first volume of a series concerned with new research contributions of the methods of logic in computer science. Contributions from leading researchers and practitioners are included in this volume. This series is designed to stimulate and sustain new, productive lines of investigation into the theory and applications of symbolic and algebraic computing techniques as it relates to logic programming and automated deduction .

The material contained in this volume discusses parallel deduction methods using connection graphs, order-sorted equational logic programming, an automated decision procedure based on the notion of the semantic tableau, an assertional programming system based on Hom clauses with equality, applications of a parallel knowledge-based system, semantic network logics for parallel computation, and a formal language for a Hoare verification system.