No label defined (Q4041013)

This is an introductory and survey book providing an acceptable account of mathematical logic applications in Computer Science and Artificial Intelligence. The book consists of separate chapters written by different authors. The first chapter (by P. I. Bystrov and V. A. Smirnov) is an introduction to first-order predicate calculus. It describes Hilbert's predicate calculus, natural deduction system, sequential calculus, Aristotelian syllogistics and its formalizations in first-order monadic predicate calculus and in Boolean algebra of classes. The second chapter (by N. N. Nepejvoda) emphasizes the strong influence of mathematical logic on logic of programs and gives a historical survey of logic applications in programming. The chapter covers logics of program description, partial and total correctness, dynamic logic, constructive and intuitionistic logics, semantics of realizability, implicant logic and formulas as types, logic of program schemes, extracting programs from constructive proofs and other topics. The third chapter (by A. M. Anisov and V. N. Stebletsova) acquaints the reader with program verification. The reasons why the correctness of programs should be proven and the very possibility and reliability of computer proofs of theorems and programs are discussed. The notions of partial and total correctness of programs are introduced and illustrated by proofs of simple programs. The chapter also contains a succinct introduction to temporal logic application to proofs of concurrent programs. The fourth chapter (by V. A. Smirnov) describes proof-search procedures for first-order predicate calculus based on Beth's semantic tableaux, analytic tables, and cut-free sequential calculus. A heuristic interactive natural deduction system with synthetic and analytic rules is also presented and exemplified. The fifth chapter (by N. A. Aleshina, I. A. Gerasimova, V. S. Mes'kov, V. I. Shalak) focuses on applications of mathematical logic in Artificial Intelligence and comprises three independent parts. The first deals with epistemic logics, a tool to represent and to process knowledge in AI systems. Different types of modal and autoepistemic logics, their semantics and axiomatizations are surveyed and compared from the viewpoint of their adequacy to capture reasoning about knowledge. The second part addresses the problem of logical inference with bounded resources. A calculus for verifying propositional formulas taking time limitations into account is constructed. The third part recounts plausible reasoning based on inductive and probabilistic logics. Several approaches to estimate the reliability of probabilistic inferences in expert systems are discussed and collated. The book will be of interest to everybody who wishes to understand current trends in mathematical logic applications in Computer Science and Artificial Intelligence, and to witness interrelations between these applications.