• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Improvement of lemma generation and reasoning strategies for automated inductive theorem proving

Research Project

Project/Area Number 16K16032
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeMulti-year Fund
Research Field Software
Research InstitutionHokkai-Gakuen University

Principal Investigator

SATO HARUHIKO  北海学園大学, 工学部, 准教授 (30543178)

Project Period (FY) 2016-04-01 – 2018-03-31
Project Status Completed (Fiscal Year 2017)
Budget Amount *help
¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2017: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2016: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Keywords定理自動証明 / 帰納的定理証明 / 補題自動生成 / 書き換え帰納法 / 項書換え系 / 形式的検証
Outline of Final Research Achievements

With the increasing importance of software systems, the need to ensure safety or correctness of them in a rigorous way is growing. Formal verification is a generic name of such a rigorous approach, where the meaning of the description of a system and of the desirable properties for the system are formalized unambiguously and we mathematically prove that the system has the properties under the formalization. For difficult proof tasks, human experts need to make proofs by hand. Since the cost for involving human experts is expensive, the improvement of automated theorem provers is one of the most important subjects for popularization of formal verification. In order to automate the proof of the type of theorems called inductive theorems, which is the class of theorems requiring mathematical (well-founded) induction to prove and hence is known to be hard to automate, in this study we propose new methods for automated lemma generation required for inductive theorem proving.

Report

(3 results)
  • 2017 Annual Research Report   Final Research Report ( PDF )
  • 2016 Research-status Report
  • Research Products

    (2 results)

All 2018 2016

All Presentation (2 results) (of which Int'l Joint Research: 2 results)

  • [Presentation] On Usefulness of Syntactically Complex Lemmas in Theory Exploration for Inductive Theorems2018

    • Author(s)
      Haruhiko Sato and Masahito Kurihara
    • Organizer
      The International MultiConference of Engineers and Computer Scientists 2018
    • Related Report
      2017 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Discovering Inductive Theorems Using Rewriting Induction2016

    • Author(s)
      Haruhiko Sato and Masahito Kurihara
    • Organizer
      The 2016 IEEE International Conference on Systems, Man, and Cybernetics (SMC 2016)
    • Place of Presentation
      Intercontinental Budapest, Hungary
    • Year and Date
      2016-10-09
    • Related Report
      2016 Research-status Report
    • Int'l Joint Research

URL: 

Published: 2016-04-21   Modified: 2019-03-29  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi