Algorithm-Sketch of

1

Find prenex P of S.

2

Set K = 1.

3

Carry out step K of .

4

Decide whether set of q-f sentences is satisfiable or not.

a

If only sentence letters in , use truth-table approach.

b

If other terms appear in , then

i

Find number of distinct terms in .

ii

Enumerate diagrams.

iii

Check satisfiability of on each diagram.

5

If YES, stop and write `Yes.'

6

If NO, set K = K + 1.

7

GOTO line 3.

• About this document ...