• DocumentCode
    3242751
  • Title

    Monotone simulations of nonmonotone proofs

  • Author

    Atserias, Albert ; Galesi, Nicola ; Pudlak, Pavel

  • Author_Institution
    Univ. Politecnica de Catalunya, Barcelona, Spain
  • fYear
    2001
  • fDate
    2001
  • Firstpage
    36
  • Lastpage
    41
  • Abstract
    We show that an LK proof of size m of a monotone sequent (a sequent that contains only formulas in the basis ∧, V) can be turned into a proof containing only monotone formulas of size mO(log m) and with the number of proof lines polynomial in m. Also we show that some interesting special cases, namely the functional and the onto versions of PHP and a version of the matching principle, have polynomial size monotone proofs
  • Keywords
    computational complexity; process algebra; simulation; theorem proving; LK proof; functional pigeon hole principle version; matching principle; monotone formulas; monotone sequent; monotone simulations; nonmonotone proofs; onto pigeon hole principle version; polynomial size monotone proofs; proof lines; Boolean functions; Calculus; Circuit simulation; Complexity theory; Polynomials;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Computational Complexity, 16th Annual IEEE Conference on, 2001.
  • Conference_Location
    Chicago, IL
  • Print_ISBN
    0-7695-1053-1
  • Type

    conf

  • DOI
    10.1109/CCC.2001.933870
  • Filename
    933870
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3242751