単純型項書換え系における定理自動証明系HOPSYS  [in Japanese] Automated Program Verification with HOPSYS  [in Japanese]

Search this Article

Author(s)

Abstract

本稿では,高階関数を取り扱える定理自動証明系HOPSYS (Higher-Order Proving System)を紹介する.HOPSYSでは仕様をMLやHaskellなどの関数型言語に似た構文で記述し,それを単純型項書換え系とみなして様々な検証や自動証明を行うことができる.また,利便性を高めるためWebユーザーインターフェースが用意されており,HOPSYSの機能のうち停止性証明,Knuth-Bendix完備化手続き,帰納的定理の自動証明が実行できる.本稿では特にHOPSYSで実現されている帰納的定理の自動証明についてのいくつかの証明法やリップリングと呼ばれる補題探索手法などを紹介する.

In this paper, we introduce the system HOPSYS (Higher-Order Proving System), an automated theorem prover that can treat higher-order functions. An input of HOPSYS is a specification written in ML/Haskell-like language. HOPSYS can verify many kinds of property and can prove theorems automatically. HOPSYS has a WUI in which we can use verifing termination property, KB completion procedure, and automatic reasoning of inductive theorems. We also introduce automatic reasoning of inductive theorems mainly, and explain some techniques for proving inductive theorems and finding lemmas by rippling.

Journal

  • IEICE technical report

    IEICE technical report 106(426), 7-12, 2006-12-07

    The Institute of Electronics, Information and Communication Engineers

References:  12

Codes

  • NII Article ID (NAID)
    110006163165
  • NII NACSIS-CAT ID (NCID)
    AN10013287
  • Text Lang
    JPN
  • Article Type
    ART
  • ISSN
    09135685
  • NDL Article ID
    8602640
  • NDL Source Classification
    ZN33(科学技術--電気工学・電気機械工業--電子工学・電気通信)
  • NDL Call No.
    Z16-940
  • Data Source
    CJP  NDL  NII-ELS 
Page Top