12.9. Inductive reasoning

Solution 9.3 

Determine the \(\theta\)-LGG of the following two clauses:

reverse([2,1],[3],[1,2,3]):-reverse([1],[2,3],[1,2,3]).
reverse([a],[],[a]):-reverse([],[a],[a]).

reverse([H|T],A,[RH|RT]):-reverse(T,[H|A],[RH|RT]).

This is the recursive clause in the version with accumulator of the reverse/3 predicate (Section 3.6), with one small difference: here, the third argument is required to be a non-empty list (which it always is). Notice that this clause is not strictly constrained, and cannot be inferred by the induction programs in Sections 9.2 and 9.3 (see also Exercise 9.4).