• DocumentCode
    2090276
  • Title

    Chaining techniques for automated theorem proving in many-valued logics

  • Author

    Ganzinger, Harald ; Sofronie-Stokkermans, Viorica

  • Author_Institution
    Max-Planck-Inst. fur Inf., Saarbrucken, Germany
  • fYear
    2000
  • fDate
    2000
  • Firstpage
    337
  • Lastpage
    344
  • Abstract
    We apply chaining techniques to automated theorem proving in many-valued logics. In particular, we show that superposition specializes to a refined version of the many-valued resolution rules introduced by Baaz and Fermuller, and that ordered chaining can be specialized to a refutationally complete inference system for regular clauses
  • Keywords
    multivalued logic; theorem proving; automated theorem proving; chaining techniques; inference system; many-valued logics; many-valued resolution rules; superposition; Constraint theory; Encoding; Multivalued logic; Postal services; Terminology;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Multiple-Valued Logic, 2000. (ISMVL 2000) Proceedings. 30th IEEE International Symposium on
  • Conference_Location
    Portland, OR
  • ISSN
    0195-623X
  • Print_ISBN
    0-7695-0692-5
  • Type

    conf

  • DOI
    10.1109/ISMVL.2000.848641
  • Filename
    848641