
## 2.1 Conventions And Assumptions

l constant, function and predicate s mbols in programs begin with lower case letters, while capital letters are reserved for variables. races are used to denote unordered sets
), and angle brackets are used for ordered se uences (e.g.,
(e.g.,
).

arallel lines ( ) denote concatenations of ordered se uences of subgoals. hen speaking about abstract subgoals (and not named predicates of concrete programs), we denote separate
), ordered se  uences of subgoals b  capitali ed  vectors sssees and the content of the content of the content.

s ), and sets of subgoals b  calligraphic capitals (
). ( ) denotes the set of all permutations of  .

e assume that the programs we work with are written in pure Prolog, i.e., without cut operators, meta logical or e tra logical predicates. Iternativel , we can assume that onl pure rolog sub se uences of subgoals are sub ect to ordering. or e ample, given a rule of t he form l 2 -     3 4 5 onl its final part 1 4 5 6 can be ordered (without a ecting the solution set).

In this work we focus upon the task of finding all the solutions to a set of subgoals.

## 2.2  Ordering Of Subgoals In Logic Programs

logic program is a set of clauses l

## 2

(
)
n are literals (predicates with arguments). To use such a clause for w here l proving a goal that matches , we must prove that all s hold simultaneousl , under consistent bindings of the free variables. solution is such a set of variable bindings. The solution set of a goal is the bag of all its solutions created b  its program.

compulation rule defines which subgoal will be proved ne t. In  rolog, the compu tation rule alwa s selects the leftmost subgoal in a goal. If a subgoal fails, backtracking is performed the proof of the previous subgoal is re entered to generate another solution.

or a detailed definition of the logic inference process, see   lo d (19 7).

Theorem 1 The solution set of a set of subgoals does not depend on the order of their execution.

hen we are looking for all solutions, the solution set does not depend on the P roof:
computation rule chosen (Theorems 9. and 1 . in  lo d, 19 7). ince a transposition of subgoals in an ordered se  uence can be regarded as a change of the computation rule (the sssent of the state of the state of the state of the state of the state of the state of the state of the state of the state.

set.

□
This theorem implies that we ma reorder subgoals during the proof derivation. et the efficiency of the derivation strongl depends on the chosen order of subgoals. The following e ample illustrates how two di erent orders can lead to a large di erence in e ecution e cienc .