Abstract
The method of Socratic proofs (SP-method) simulates the solving of logical problem by pure questioning. An outcome of an application of the SP-method is a sequence of questions, called a Socratic transformation. Our aim is to give a method of translation of Socratic transformations into trees. We address this issue both conceptually and by providing certain algorithms. We show that the trees which correspond to successful Socratic transformations—that is, to Socratic proofs—may be regarded, after a slight modification, as Gentzen-style proofs. Thus proof-search for some Gentzen-style calculi can be performed by means of the SP-method. At the same time the method seems promising as a foundation for automated deduction.
Similar content being viewed by others
References
McAllester D., Givan R.: Taxonomic syntax for first order inferences. Journal of ACM 40(2), 246–283 (1993)
Avron, A., The method of hypersequents in the proof theory of propositional non-classical logics, in W. Hodges et al. (eds.), Logic: Foundations to Applications, Oxford Science Publications, Clarendon Press, Oxford, 1996, pp. 1–32.
Buss, S.R. (ed.): Handbook of Proof Theory. Elsevier, Amsterdam (1998)
Heeffer A.: Automated Theorem Prover for CL and CLuN Based on the Method of Socratic Proofs. Ghent University, Centre for Logic and Philosophy of Science (2003)
Leszczyńska, D., Socratic proofs for some normal modal propositional logics, Logique et Analyse 185–188, 259–285, 2004.
Leszczyńska D.: The Method of Socratic Proofs for Normal Modal Propositional Logics. Adam Mickiewicz University Press, Poznań (2007)
Leszczyńska-Jasion D.: The method of socratic proofs for modal propositional logics: K5, S4.2, S4.3, S4M, S4F, S4R and G. Studia Logica 89(3), 371–405 (2008)
Leszczyńska-Jasion D.: A loop-free decision procedure for modal propositional logics K4, S4 and S5. Journal of Philosophical Logic 38(2), 151–177 (2009)
Leszczyńska-Jasion, D., On Determining Modal Sequent Proofs by Socratic Proofs, Research Report, Adam Mickiewicz University, Institute of Psychology, Chair of Logic and Cognitive Science, 2010.
Negri S., von Plato J.: Structural Proof Theory. Cambridge University Press, Cambridge (2001)
Skura T.: Intuitionistic socratic procedures. Journal of Applied Non-Classical Logics 15(4), 453–464 (2005)
Smullyan R.M.: First-Order Logic. Springer-Verlag, Berlin (1968)
Troelstra A.S., Schwichtenberg H.: Basic Proof Theory (2nd ed.). Cambridge University Press, Cambridge (2000)
Urbański, M., Socratic Proofs for Some Temporal Logics, Research Report, Adam Mickiewicz University, Institute of Psychology, Chair of Logic and Cognitive Science, 2005.
Wiśniewski A.: Erotetic implications. Journal of Philosophical Logic 23(2), 174–195 (1994)
Wiśniewski A.: The Posing of Questions: Logical Foundations of Erotetic Inferences. Kluwer Academic Publishers, Dordrecht/Boston/London (1995)
Wiśniewski A.: The logic of questions as a theory of erotetic arguments. Synthese 109(2), 1–25 (1996)
Wiśniewski A.: Questions and inferences. Logique et Analyse 173–175, 5–43 (2001)
Wiśniewski A.: Socratic proofs. Journal of Philosophical Logic 33(3), 299–326 (2004)
Wiśniewski A., Vanackere G., Leszczyńska D.: Socratic proofs and paraconsistency: a case study. Studia Logica 80(2–3), 433–468 (2005)
Wiśniewski A., Shangin V.: Socratic proofs for quantifiers. Journal of Philosophical Logic 35(2), 147–178 (2006)
Author information
Authors and Affiliations
Corresponding author
Additional information
Presented by Andrzej Indrzejczak
Rights and permissions
About this article
Cite this article
Leszczyńska-Jasion, D., Urbański, M. & Wiśniewski, A. Socratic Trees. Stud Logica 101, 959–986 (2013). https://doi.org/10.1007/s11225-012-9404-0
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-012-9404-0