ERRATA

for "SAT solver of Howe & King as a logic program", by W. Drabent, 
Logic Programming Newsletter, 24(2), June 2011,
and for the first version of its extension
"Logic + control: An example of program construction"
http://arxiv.org/abs/1110.4978v1 (version 1 of 2011).


There is an error in the specification.  The definition of L1 (page 2)
should be modified.  For the purpose of the simple program of Section 2
it should be:

  Let  L_1  be the set of ground terms of the form
  [t1-u1,...,tn-un|s]  (n>0), where  ti=ui  for some i.

For the purpose of the main program, Section 4, it should be

  Let  L_1  be the set of ground terms of the form
  [t-t], or
  [t1-u1,...,tn-un|s]  (n>1), where  ti=ui  for some i.


Also, some atoms should be excluded from the specification of
update_watch/5 (p.9).  The specified atoms should be 

  update_watch( v1,p1,v2,p2,s )  where
				 v1=p1, or
				 [p2-v2|s]  is in  L1

(The error was discovered by checking some of the simple proof details
left to the reader.)

................................................................

The following corrections are needed in the level mappings (p. 6 and
footnote 10 of the extended paper).

In defining  |sat(t,t')|,

   |t'|  should be replaced by  listsize(t').

It should be 

   |elim_var(t)| = listsize(t).

Where  listsize([h|t]) = 1 + listsize(t),  and  listsize(s) = 0  for a
term whose main symbol is not  [ | ].


2012-03-23