Business Profile

Mentor® is an environment with resources that support machine learning, information organization and knowledge acquisition, and therefore it allows the development of several intelligent applications. In order to do so, it has an inference machine which allows to perform deductions over one or more knowledge bases, a large amount of primitives from a Prolog-like programming language and a pattern matching process.

Technical Profile

Mentor® is an flexible and robust automatic theorem prover. One of the techniques employed on its development is the backtrack path, which divides the original problem into smaller problems. By using Herbrand results, it is possible to transform the first order logic clauses into propositional logic clauses. The quantifiers of such clauses are explicitly handled just at the beginning of tasks, that is, at the beginning of the deductions.

During deductions, it is used the resolution process with refutation, which denies the original questioning, and by combining unification and resolution it reaches the empty clause, that is, an affirmative answer. When such empty clause is not obtained, even though following all possible paths, then the answer is no.

The theorem prover uses the linear strategy, whose completeness proof is easily found at specialized literature. If there is a clause that cannot be solved by any clauses from the knowledge base, it is performed a backtrack to the previous clause. Then, a new attempt of resolution is performed by using any other clause that has not been solved yet, starting a new path. If this new path reaches an dead end, a new backtrack is performed and so on.

Despite elegant, the basic resolution procedure produces a great amount of intermediate clauses (in fact secondary problems), and it is not able to avoid the combinatorial explosion. Hence, it is necessary to use tuning techniques in order to limit the number of clauses to be checked.

The mechanism of clauses selection is responsible for establishing an resolution strategy, and it resolves just two clauses at once so that it can limit the number of possible alternatives. However, there still might exists a large quantity of resolution possibilities, among those, just a few, or even none, would lead to an empty clause. Thus, it was also created an mechanism to bound the deductions depth.

The prover pushes the input clauses, and then pushes the clause representing the question negation followed by the obtained resolvent. The retrospective path is easily obtained by popping the clauses. The process ends when is reached an contradiction, which means an affirmative answer; or when the first clause of the question negation is popped with no new paths, meaning a process fault and consequently an negative answer.