The ``resolution'' describes a general method of reasoning within the first order logic. The theoretical description of the method allows for different realizations, called ``resolution strategies'', reflecting different compromises between the performance and the generality. The ``more general'' strategies are very costly in calculation time and require a memory space, which limits the usability of the method. On the other hand, in more specific cases, by using adapted strategies and by distributing the calculations among several processors, one obtains quite interesting results.

During my 8 month contract at the University of Quebec in Hull (UQAH),
Canada, I have developed a parallel program for resolution. Apart
from a didactic aspect of the program, which consists of helping to
understand the first order logic, its practical interest has been
proven within the system `fun-tools`. Developed at UQAH,
`fun-tools` assists the user in the creation of technical
documentation for different phases of the development of computer
systems. Several documents, being part of such a specification, have a
mathematical character. My program permits the verification of the
completeness and the consistence of certain parts of these documents.

This work has been published in a technical report [FI97].