Prolog

LOGIC, PROGRAMMING AND PROLOG (2ED)
Ulf Nilsson and Jan Maluszy´ski n

Copyright c 2000, Ulf Nilsson and Jan Maluszy´ski. The book may be downn loaded and printed for personal use only provided that the text (1) is not altered in any way, and (2) is accompanied by this copyright notice. The book may also be copied and distributed in paper-form for non-profit use only. No other form ofdistribution is allowed. It is not allowed to distribute the book electronically. This book was previously published by John Wiley & Sons Ltd. The book was originally published in 1990 with the second edition in 1995. The copyright was reverted back to the authors in November 2000. For further information about updates and supplementary material please check out the book web-site athttp://www.ida.liu.se/~ulfni/lpp or contact the authors at ulfni@ida.liu.se and janma@ida.liu.se.

Contents

Preface

ix

I

Foundations
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1
3 3 710 13 14 16 19 19 21 24 29 31 33 33 37 43 48 51 53 57

1 Preliminaries 1.1 Logic Formulas . . . . . . . . . . 1.2 Semantics of Formulas . . . . . . 1.3 Models and Logical Consequence 1.4 Logical Inference . . . . . . . . . 1.5 Substitutions . . . . . . . . . . . Exercises . . . . . . . . . . . . . 2 Definite Logic Programs 2.1 Definite Clauses . . . . . . . . . 2.2 Definite Programs and Goals . 2.3The Least Herbrand Model . . 2.4 Construction of Least Herbrand Exercises . . . . . . . . . . . . 3 SLD-Resolution 3.1 Informal Introduction . . . . . 3.2 Unification . . . . . . . . . . . 3.3 SLD-Resolution . . . . . . . . . 3.4 Soundness of SLD-resolution . 3.5 Completeness of SLD-resolution 3.6 Proof Trees . . . . . . . . . . . Exercises . . . . . . . . . . . .

. . . . . . . . . . . . . . .Models . . . . . . . . . . . . v . . . . . . . . . . . . . . . . . . . . . . . . . . . .

vi 4 Negation in Logic Programming 4.1 Negative Knowledge . . . . . . . . . . . 4.2 The Completed Program . . . . . . . . . 4.3 SLDNF-resolution for Definite Programs 4.4 General Logic Programs . . . . . . . . . 4.5 SLDNF-resolution for General Programs 4.6 Three-valued Completion . . . . . . . . 4.7Well-founded Semantics . . . . . . . . . Exercises . . . . . . . . . . . . . . . . .

Contents 59 59 61 65 67 70 75 77 84 87 87 93 97

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

.. . . . . . .

. . . . . . . .

. . . . . . . .

5 Towards Prolog: Cut and Arithmetic 5.1 Cut: Pruning the SLD-tree . . . . . . . . . . . . . . . . . . . . . . . . 5.2 Built-in Arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

II

Programming in Logic
. . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

99
101 101 103 104 107 109 114 116 119 119 119 129 131 135 135 136 141 143 144 146 146 149 149 153 154 155 161

6 Logic and Databases 6.1 Relational Databases . . . . . . . . . ....