The paper

L. Pinto & R. Dyckhoff, Loop-free construction of counter-models for intuitionistic propositional logic, in: Symposia Gaussiana, Conf. A, Eds.: Behara/Fritsch/Lintz, Walter de Gruyter & Co, Berlin, New York, 1995, pp 225-232..

should be amended by the addition (to the refutation calculus) of a rule for dealing with formulae of the form F->B in the antecedent (where "F" is absurdity, falsum). The rule is

   			  Gamma =/=> Delta
			----------------------
			Gamma, F->B =/=> Delta

The omission of a corresponding rule from the proof calculus is deliberate: it is an instance of the admissible rule of weakening.