Natural Style for Resolution Proofs in Theorema

The proofs generated by clausa reasoners are often too long and hard to follow by the user (even if experienced), because most of the structure of the initial problem is not expressed by the clausal formula. For this reason, it is very important, especially for practical applications, to express the proofs in a more natural style. This paper analyzes the method suggested by [Meier], namely to perform the transformation on the proofs obtained by resolution at the assertion level. More precise, the emphasis was on integrating the algorithms suggested by [Meier] in the Theorema system which is an automated theorem prover built on Mathematica. A first step was to bring the proofs generated by a resolution prover- in this case Otter- in a uniform representation- i.e. refutation graphs