crossword puzzle with prolog

Currently I am doing a Prolog tutorial.

There is an exercise to solve a crossword puzzle with 5 words.

My Problem is that Prolog stops unification for my solution at a very early point.

It looks like that:

And there is a small knowledge base given:

   word(astante,  a,s,t,a,n,t,e). 
   word(astoria,  a,s,t,o,r,i,a). 
   word(baratto,  b,a,r,a,t,t,o). 
   word(cobalto,  c,o,b,a,l,t,o). 
   word(pistola,  p,i,s,t,o,l,a). 
   word(statale,  s,t,a,t,a,l,e).

To solve that task I have a predicate crossword/6.

So I have thought that the predicate crossword must contain 6 words that are made of variables and at every field where two words cross I have set there the same variable.

crossword(word(H1, A1, B1, C1, D1, E1, F1, G1),
          word(H2, A2, B2, C2, D2, E2, F2, G2),
          word(H3, A3, B3, C3, D3, E3, F3, G3),
          word(V1, _1, B1, _2, B2, _3, B3, _4),
          word(V2, _5, D1, _6, D2, _7, D3, _8),
          word(V3, _9, F1, _10, F2, _11, F3 _12)).

In SWI-Prolog I have typed the following request:

?- crossword(H1, H2, H3, V1, V2, V3).

So I have asked for the solution of a crossword puzzle.

The result I get is like that:

H1 = word(_720, _722, _724, _726, _728, _730, _732, _734),
H2 = word(_738, _740, _742, _744, _746, _748, _750, _752),
H3 = word(_756, _758, _760, _762, _764, _766, _768, _770),
V1 = word(_774, _776, _724, _780, _742, _784, _760, _788),
V2 = word(_792, _794, _728, _798, _746, _802, _764, _806),
V3 = word(_810, _812, _732, _816, _750, _820, _768).

Question: Why does Prolog stop unification at such a early point ? And why doesn't it return any solution?

Your code declares a simple fact: there is a crossword/6 predicate whose arguments are word/8 predicates, and some of the arguments of the word/8 predicates are the same. In particular, since crossword/6 is declared as a simple fact, there's no relationship between the word/8 predicates in the crossword/6 declaration and the knowledge base (just like the fact for "astoria" doesn't constrain the fact for "astante").

Instead, only the words themselves are simple facts:

word(astante,  a,s,t,a,n,t,e).
word(astoria,  a,s,t,o,r,i,a).
word(baratto,  b,a,r,a,t,t,o).
word(cobalto,  c,o,b,a,l,t,o).
word(pistola,  p,i,s,t,o,l,a).
word(statale,  s,t,a,t,a,l,e).

Because these are simple facts with no conditions, we can always prove that there is a word/8 predicate whose first argument is astante/0, second argument is a/0, third argument is s/0, and so on.

What you want to say is that the six words form a valid solution if other things are true of those words:

crossword( H1, H2, H3, V1, V2, V3 ) :-
  <conditions for a successful crossword solution>.

Next, define the conditions for crossword/6 so that a valid solution is one in which the variables unify with the first argument of word/8 predicates if the third, fifth, and seventh arguments of those word/8 arguments unify with each other in the right way.

For an (incomplete) example, I can say I have a valid cross-word solution if the second letter of H1 is the second letter of V1, and the sixth letter of H1 is the second letter of V3:

crossword( H1, H2, H3, V1, V2, V3 ) :-
  word( H1, _, TL, _, _, _, TR, _ ),
  word( V1, _, TL, _, _, _, _, _ ),
  word( V3, _, TR, _, _, _, _, _ ).

Here I'm using underscore _ to avoid giving names to variables whose names don't matter. I'm also using TL and TR for "top left" and "top right" to make the reasoning easier on myself. Prolog sees that we can prove crossword/6 if we can prove that there are word/8 predicates whose arguments unify in a particular way, and searches for combinations of word/8 predicates that do so. The "knowledge base" provides axioms for each possible proof.

Do you see how to complete the crossword/6 definition now? Notice that you'll need to give some of the underscore variables (called "anonymous variables") names to complete the solution, and introduce additional word/8 terms on the right-hand side of the turnstyle.