Proof Simplification in the Framework of Coherent Logic

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

• Type: Journal
• Year: 2015
• Where: CAI
• Authors: Vesna Marinkovic
• Keywords: CAI 2015, Information Technology