  We introduce a method of verifying termination of logic programs with respect
to concrete queries (instead of abstract query patterns). A necessary and
sufficient condition is established and an algorithm for automatic verification
is developed. In contrast to existing query pattern-based approaches, our
method has the following features: (1) It applies to all general logic programs
with non-floundering queries. (2) It is very easy to automate because it does
not need to search for a level mapping or a model, nor does it need to compute
an interargument relation based on additional mode or type information. (3) It
bridges termination analysis with loop checking, the two problems that have
been studied separately in the past despite their close technical relation with
each other.
