Switch to: References

Add citations

You must login to add citations.
  1. Logical omniscience as infeasibility.Sergei Artemov & Roman Kuznets - 2014 - Annals of Pure and Applied Logic 165 (1):6-25.
    Logical theories for representing knowledge are often plagued by the so-called Logical Omniscience Problem. The problem stems from the clash between the desire to model rational agents, which should be capable of simple logical inferences, and the fact that any logical inference, however complex, almost inevitably consists of inference steps that are simple enough. This contradiction points to the fruitlessness of trying to solve the Logical Omniscience Problem qualitatively if the rationality of agents is to be maintained. We provide a (...)
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Propositional Proof Systems and Fast Consistency Provers.Joost J. Joosten - 2007 - Notre Dame Journal of Formal Logic 48 (3):381-398.
    A fast consistency prover is a consistent polytime axiomatized theory that has short proofs of the finite consistency statements of any other polytime axiomatized theory. Krajíček and Pudlák have proved that the existence of an optimal propositional proof system is equivalent to the existence of a fast consistency prover. It is an easy observation that NP = coNP implies the existence of a fast consistency prover. The reverse implication is an open question. In this paper we define the notion of (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Short Proofs for Slow Consistency.Anton Freund & Fedor Pakhomov - 2020 - Notre Dame Journal of Formal Logic 61 (1):31-49.
    Let Con↾x denote the finite consistency statement “there are no proofs of contradiction in T with ≤x symbols.” For a large class of natural theories T, Pudlák has shown that the lengths of the shortest proofs of Con↾n in the theory T itself are bounded by a polynomial in n. At the same time he conjectures that T does not have polynomial proofs of the finite consistency statements Con)↾n. In contrast, we show that Peano arithmetic has polynomial proofs of Con)↾n, (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Derivability in certain subsystems of the Logic of Proofs is-complete.Robert Milnikel - 2007 - Annals of Pure and Applied Logic 145 (3):223-239.
    The Logic of Proofs realizes the modalities from traditional modal logics with proof polynomials, so an expression □F becomes t:F where t is a proof polynomial representing a proof of or evidence for F. The pioneering work on explicating the modal logic is due to S. Artemov and was extended to several subsystems by V. Brezhnev. In 2000, R. Kuznets presented a algorithm for deducibility in these logics; in the present paper we will show that the deducibility problem is -complete. (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • The complexity of the disjunction and existential properties in intuitionistic logic.Sam Buss & Grigori Mints - 1999 - Annals of Pure and Applied Logic 99 (1-3):93-104.
    This paper considers the computational complexity of the disjunction and existential properties of intuitionistic logic. We prove that the disjunction property holds feasibly for intuitionistic propositional logic; i.e., from a proof of A v B, a proof either of A or of B can be found in polynomial time. For intuitionistic predicate logic, we prove superexponential lower bounds for the disjunction property, namely, there is a superexponential lower bound on the time required, given a proof of A v B, to (...)
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Describing proofs by short tautologies.Stefan Hetzl - 2009 - Annals of Pure and Applied Logic 159 (1-2):129-145.
    Herbrand’s theorem is one of the most fundamental results about first-order logic. In the context of proof analysis, Herbrand-disjunctions are used for describing the constructive content of cut-free proofs. However, given a proof with cuts, the computation of a Herbrand-disjunction is of significant computational complexity, as the cuts in the proof have to be eliminated first.In this paper we prove a generalization of Herbrand’s theorem: From a proof with cuts, one can read off a small tautology composed of instances of (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations