Logic for Problem Solving, RevisitedThis seminal book of Computer Science is the most cited reference on the subject of programming in logic. Originally published in 1979, this now classic text was the first comprehensive attempt to define the scope of logic for problem solving. In this extended edition, Robert Kowalski revisits his classic text in the light of subsequent developments in a substantial commentary of fifty pages. This work investigates the application of logic to problem-solving and computer programming. It assumes no previous knowledge of these fields, and may be appropriate therefore as an introduction to logic, the theory of problem-solving, and computer programming. At the focal point is Computational Logic. It centers around the famous slogan: Algorithm = Logic + Control, which was coined by the author and is explained in this book. According to this view, an algorithm consists of a problem description (the logic part) and a strategy to perform useful computations on this description (the control part). This separation of concerns ideally leads to declarative programs that are simple to develop, clear to understand and easy to maintain. |
Contents
Introduction | 1 |
Representation in Clausal Form | 22 |
Horn Clause ProblemSolving | 75 |
The Procedural Interpretation of Horn Clauses | 107 |
PlanFormation and the Frame Problem | 133 |
Resolution | 147 |
The Connection Graph Proof Procedure | 163 |
Global ProblemSolving Strategies | 179 |
Conclusion | 246 |
261 | |
Errata of the 1979 Edition | 273 |
Representation in Clausal Form | 279 |
Horn Clause ProblemSolving | 285 |
PlanFormation and the Frame Problem | 291 |
The Connection Graph Proof Procedure | 298 |
Comparison of Clausal Form with Standard Form | 304 |
Comparison of Clausal Form with Standard Form | 193 |
Ifandonlyif | 210 |
Logic Change and Contradiction | 239 |
Formalisation of Provability | 311 |
317 | |
Other editions - View all
Common terms and phrases
algorithm and-or tree Append applied Artificial Intelligence assertions assumptions atoms backtracking birthday club bottom-up inference Chapter clausal form conclusion connection graph connection graph proof constant symbol contains data structures database defined definition deleted denial derived Diff equivalent event calculus example expressed Fallible form of logic formulation frame axiom function symbol given goal statement grandparent graph proof procedure Harmonia Holds clear Horn clause Horn clause programs implies inconsistent input integrity constraints John Kowalski matching substitution meta-language n-ary names natural language negation negation as failure node non-Horn clauses Noun Numb object language only-if half output Parent Parse predicate symbols procedure calls programming languages Prolog proof procedure recursive refutation relation relationship represented resolution search space search strategy semantic networks semantic tree sentence set of clauses solution solve standard form subgoals theorem-proving top-down and bottom-up top-down inference top-down search space true True q variables Zeus