Automatic proof generation in an axiomatic system for $\mathsf{CPL}$ by means of the method of Socratic proofs

DOI10.1093/jigpal/jzx057zbMath1499.03010OpenAlexW2770778970WikidataQ113818829 ScholiaQ113818829MaRDI QIDQ5384363

Aleksandra Grzelak, Dorota Leszczyńska-Jasion

Publication date: 24 June 2019

Published in: Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/jigpal/jzx057

zbMATH Keywords

Socratic proofsR-S systemerotetic calculusproof-search in axiomatic systemsRasiowa-Sikorski diagrams

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Classical propositional logic (03B05)

Related Items

Rasiowa-Sikorski deduction systems with the rule of cut: a case study, The Method of Socratic Proofs Meets Correspondence Analysis, CALCULIZING CLASSICAL INFERENTIAL EROTETIC LOGIC