• DocumentCode
    3493289
  • Title

    Theorem proving based on the partial instatiation technique

  • Author

    Yamamoto, Masahito ; Ohyanagi, Toshio ; Ohuchi, Azuma

  • Author_Institution
    Fac. of Eng., Hokkaido Univ., Sapporo, Japan
  • fYear
    1995
  • fDate
    26-28 Jul 1995
  • Firstpage
    1183
  • Lastpage
    1186
  • Abstract
    We present a new theorem proving procedure based on the partial instantiation technique, which is developed by Jeroslow. The proposed procedure is applicable to clausal form formulas in the first-order logic, as well as other resolution-based methods. We also show its completeness, i.e., it can verify that a given set of clauses is unsatisfiable if indeed it is unsatisfiable
  • Keywords
    artificial intelligence; formal logic; theorem proving; clausal form; completeness; first-order logic; partial instatiation; resolution-based methods; satisfiability problem; theorem proving; Bismuth; Cost accounting; Logic;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    SICE '95. Proceedings of the 34th SICE Annual Conference. International Session Papers
  • Conference_Location
    Hokkaido
  • Print_ISBN
    0-7803-2781-0
  • Type

    conf

  • DOI
    10.1109/SICE.1995.526653
  • Filename
    526653
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3493289