• DocumentCode
    3037814
  • Title

    Correctness of multiplicative proof nets is linear

  • Author

    Guerrini, Stefano

  • Author_Institution
    Dipt. di Sci. dell´´Inf., Rome Univ., Italy
  • fYear
    1999
  • fDate
    1999
  • Firstpage
    454
  • Lastpage
    463
  • Abstract
    We reformulate Danos contractibility criterion in terms of a sort of unification. As for term unification, a direct implementation of the unification criterion leads to a quasi-linear algorithm. Linearity is obtained after observing that the disjoint-set union-find at the core of the unification criterion is a special case of union-find with a real linear time solution
  • Keywords
    formal logic; theorem proving; Danos contractibility; disjoint-set union-find; multiplicative proof nets; term unification; unification; Computer science; Ear; Educational institutions; Electrical capacitance tomography; Inspection; Linearity; Logic; Remuneration; Switches; Tree graphs;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1999. Proceedings. 14th Symposium on
  • Conference_Location
    Trento
  • ISSN
    1043-6871
  • Print_ISBN
    0-7695-0158-3
  • Type

    conf

  • DOI
    10.1109/LICS.1999.782640
  • Filename
    782640
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3037814