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].