Proof Simplification in the Framework of Coherent Logic

Abstract

The problem of proof simplification draws a lot of attention to itself across various contexts. In this paper, we present one approach for simplifying proofs constructed in the framework of coherent logic. This approach is motivated by the need for filtering-out "clean'' and short proofs from proof-traces, which typically contain many irrelevant steps, and which are generated by automated theorem provers - in this case, theorem provers based on coherent logic. Such "clean'' proofs can then be used for producing readable proofs in natural-language form. The proof simplification procedure consists of three transformation steps. The first one is based on the elimination of inference steps which are irrelevant for the present proof, also allowing some irrelevant branchings to be eliminated, the second one consists of lifting-up steps through the branching steps, followed by elimination of repeated steps, while the third one serves to convert proof fragments into the reductio ad absurdum form, if possible. In contrast to general simplification procedures, our proof simplification procedure is specific for a fragment of first order logic and therefore simple and easy to implement, and allows simple generation of object level proofs. We proceed to prove that this procedure is correct and terminating, and also that it never increases the size of a proof. Finally, we implement the proof simplification procedure, and provide several example proofs.