Facebook Instagram Twitter RSS Feed PodBean Back to top on side

Proof Simplification in the Framework of Coherent Logic

In: Computing and Informatics, vol. 34, no. 2
V. Marinković

Details:

Year, pages: 2015, 337 - 366
Keywords:
Proof simplification, coherent logic, readable proofs, automated theorem provers, reductio ad absurdum
About article:
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.
How to cite:
ISO 690:
Marinković, V. 2015. Proof Simplification in the Framework of Coherent Logic. In Computing and Informatics, vol. 34, no.2, pp. 337-366. 1335-9150.

APA:
Marinković, V. (2015). Proof Simplification in the Framework of Coherent Logic. Computing and Informatics, 34(2), 337-366. 1335-9150.