Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Studia Logicaarrow_drop_down
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao
Studia Logica
Article . 2012 . Peer-reviewed
License: Springer TDM
Data sources: Crossref
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao
zbMATH Open
Article . 2013
Data sources: zbMATH Open
DBLP
Article
Data sources: DBLP
versions View all 3 versions
addClaim

This Research product is the result of merged Research products in OpenAIRE.

You have already added 0 works in your ORCID record related to the merged Research product.

Socratic Trees

Socratic trees
Authors: Dorota Leszczynska-Jasion; Mariusz Urbanski; Andrzej Wisniewski;
Abstract

The paper is concerned with proof-theoretic aspects of the method of Socratic transformations. It is founded on inferential erotetic logic developed by Wiśniewski and based on the idea of solving logical problems by questioning. A question in this framework is formulated as a finite list of sequents with one formula in the succedent. The key notion is that of a Socratic transformation of initial question into simpler ones by means of suitable rules. The method was already applied succesfully by Wiśniewski and his collaborators to many nonclassical logics, including modal and paraconsistent logics. In this paper, a system of Socratic proofs for classical logic is examined. Any Socratic transformation (a proof in particular) is similar to a proof tree in hypersequent calculi. However, the rules of the system are dual, i.e. whereas hypersequents are meant as metalogical disjunctions over sequents, questions are meant as conjunctions. Due to that, Socratic transformations avoid branching. In the paper, it is shown that every Socratic transformation may be translated into a proof tree of annotated sequents, called Socratic tree, where branching is present but we avoid rewriting of sequents which are not active in some deductive step. This leads to introduction of some form of cut-free sequent calculus for classical logic with rules introducing negated formulae, double negations and special rules for introduction of disjunction (negated conjunction) to succedent. All steps of the transformation are presented in detail and with formal algorithms, including an algorithm for reduction of the complexity of obtained trees. One may find this method an interesting alternative to other solutions applied in automated deduction. The paper clarifies the relationship of Socratic transformations to sequent calculus. It may be of interest for students in proof theory and automated deduction.

Related Organizations
Keywords

Mechanization of proofs and logical operations, sequent calculi, erotetic logic, Structure of proofs, Socratic transformations, proof theory, automated deduction

  • BIP!
    Impact byBIP!
    selected citations
    These citations are derived from selected sources.
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    13
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Top 10%
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
Powered by OpenAIRE graph
Found an issue? Give us feedback
selected citations
These citations are derived from selected sources.
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
13
Average
Top 10%
Average
Upload OA version
Are you the author of this publication? Upload your Open Access version to Zenodo!
It’s fast and easy, just two clicks!