Résumé d'Implementation of logics ... :
Logic bas always formed an important part of the foundations of computer science. Implicitly, logic is used in nearly all sub-fields of computer science and computer engineering, from very concrete hardware to purely abstract arguments. Explicitly represented logical constructs have been used to model human reasoning in attempts to develop better intelligent systems, as a declarative programming language to specify and solve problems, and for a large number of other tasks. Many logics are widely recognised as providing powerful tools for the unambiguous description of important and practically relevant problems. The practical application of logics for real-world problems, however, is held back by the fact that reasoning in many logics is a very complex task. For the most useful logics, the validity problem and the implication problem are either undecidable, or fall into hard complexity classes, yet, increasingly efficient implemented systems are being developed. The papers in Implementation of logics present a fine cross-section of current research on the implementation of logical tools for a variety of standard and non-standard deduction tasks, and their applications. Techniques featured include binary decision diagrams for modal logic, compilation of normal Prolog programs with stable semantics, proof checking for Kleene algebras, approximate database technology, technologies for studying the lambda calculus and substitution calculi, rule-based programming, and inductive theorem proving.