Trigger Technique in an Infinite Herbrand Universe

The trigger technique is an important mechanism in automated deduction. The technique is to trigger the resumption of a derivation which has been stopped due to a technical reason, and therefore lead to the completion of the derivation. The soundness of the technique, however, limits it to be applied to logic programs which have a finite (Herbrand) universe and, this has significantly restricted its application scope. This paper analyses the technique and explores the possibility of applying the technique to logic programs with an infinite universe, and hence expands its applications scopehis electronic document is a "live" template. The various components of your paper [title, text, heads, etc.] are already defined on the style sheet, as illustrated by the portions given in this document.