| - Up - | Next >> |
Now let's turn to an implementation of what we've learnt. Basically, we only have to do two things:
We have to devise data structures for handling tableaux.
We have to represent the tableaux inference rules in Prolog.
As regards the first task, our decision is this: We do not represent tableaux explicitely. Rather, we use Prolog's backtracking mechanism to ``crawl along'' the tableaux under construction. This makes the second task almost trivial - really all we have to do is translate our inference rules into Prolog. The resulting program is somewhat different from what you might expect if you think about constructing tableaux with pen and paper. Nevertheless it's elegant and easily implemented.
| - Up - | Next >> |