This Web page contains an ABSTRACT of the publication and information on the CONTEXT in which the publication has appeared.
The presentation has three goals in mind. For one, it gives an introduction to various calculi for first-order logic which should provide the reader with a good sense of them. Secondly, it aims at clarifying the relationships among these calculi, including resolution, especially in view of automating deduction. To be specific, we consider Hilbert and Gentzen calculi, tableau calculi, connection calculi, and resolution including its extensions. With such a broader view of automated deduction in mind several issues present themselves in a new light. The third goal, therefore, is a presentation of the issues relevant for the automation of deduction. In particular, we discuss several aspects of controlling the search for a proof, we consider restrictions as well as extensions of first-order logic, and we present proof methods and heuristics for special theories.
This publication is Chapter 3 of Volume 1 of the Handbook of Logic in Artificial Intelligence and Logic Programming. The Handbooks of Logic in Computer Science and of Logic in Artificial Intelligence and Logic Programming, edited by Dov M. Gabbay and published by Oxford University Press, comprise the following subjects:
Volume 1 of the Handbook of Logic in Artificial Intelligence and Logic Programming consists of the following chapters.
The publisher gives the following description of this volume.
Logic is now widely recognized to be one of the foundational disciplines of computing and has found applications in virtually all aspects of the subject, from software engineering and hardware to programming languages and artificial intelligence. This Handbook has been created in response to the growing need for an in-depth survey of the applications of logic in AI and computer science. The Handbook of Logic in Artificial Intelligence and Logic Programming will be published in five volumes. Each volume provides a combination of authoritative exposition, comprehensive survey, and fundamental research exploring the underlying unifying themes in the various areas. this first volume presents the logical foundations and deduction methodologies extensively used in AI.