Automatic proof generation in an axiomatic system for $\mathsf{CPL}$ by means of the method of Socratic proofs
Aleksandra Grzelak, Dorota Leszczyńska-Jasion · Logic Journal of IGPL · 2017
The aim of this article is to describe an algorithm for the automatic generation of proofs in an axiomatic system for Classical Propositional Logic. The idea of the algorithm was taken from a book by Helena Rasiowa and Roman Sikorski [31], where the authors suggest using the method of diagrams to automatically obtain proofs in Classical Propositional Logic. However, in this article the method of diagrams developed by Rasiowa and Sikorski was replaced by a right-sided erotetic calculus developed by Andrzej Wiśniewski. Erotetic calculi have been used before in designing similar algorithms. The proofs are presented together with the estimations of their lengths, widths and sizes — measures introduced for the purposes of the article. The estimations are then used to derive the conclusion that the axiomatic system simulates polynomially the erotetic calculus.