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

Automated Deduction and Reduction Orders

Research Project

Project/Area Number 22K11900
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Review Section Basic Section 60010:Theory of informatics-related
Research InstitutionJapan Advanced Institute of Science and Technology

Principal Investigator

廣川 直  北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (50467122)

Project Period (FY) 2022-04-01 – 2026-03-31
Project Status Granted (Fiscal Year 2023)
Budget Amount *help
¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2025: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2024: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2023: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2022: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Keywords自動演繹 / 項書換え / 定理自動証明 / 停止性 / 完備化 / 簡約順序
Outline of Research at the Start

現代の情報社会においてソフトウェアバグは深刻な被害をもたらす。そのためソフトウェアの正しさの保証は社会的な課題となっている。しかし現実社会で用いられるシステムは巨大なものが多く、人手による検証は現実的ではない。そのため必要とされる数学的な証明を自動化する効率的な技法が必要不可欠である。1989年に登場した順序付き完備化は、現在最も成功している等式論理の自動証明技法である。この証明能力と証明速度を向上させる理論と自動化技法を研究する。

Outline of Annual Research Achievements

現代の情報社会においてソフトウェアバグは深刻な被害をもたらすため、ソフトウェアの正しさの保証は社会的な課題となっている。しかし現実社会で用いられるシステムは巨大なものが多く、数学的証明を効率的に自動化する技法が必要不可欠となる。「順序付き完備化」と「書換え帰納法」は、現在最も成功している等式論理の自動証明技法である。これらの証明能力と証明速度を向上させる理論と自動化技法を構築することが本研究の目標である。令和4年度に引き続き、(A)「順序選択問題の解決」、(B)「強力な簡約順序の開発」、「項書換えの合流性証明技法」の三つに取り組んだ。
(A) 結合律 (x+y)+z=x+(y+z) と交換律 x+y=y+x を満たす演算子はAC演算子と呼ばれる。数学定理やソフトウェア検証における多くの命題には算術が関与し、AC演算子を扱う必要がある。自動演繹の基本は、0+x=x のような等式を計算規則 0+x→x として扱い数式を単純化することにあるが、AC演算子は0+x→x+0→0+x→…のように素朴な単純計算方法では停止しないため、それらを扱う「AC完備化」と呼ばれる手法が研究されている。本研究では既存の3つのAC完備化を調査し、それらの証明能力が階層を為すことを解明した。
(B) 現在多くの定理自動証明システムは簡約順序と呼ばれる順序を用いて、等式を計算規則にする際の矢印の向きを決めている。AC演算子を扱え、かつ理論的な扱いが容易な新たな簡約順序を開発した。
(C) 合流性は計算結果の一意性を保証する性質であり、等式の自動証明を計算によって行うことを可能にする。令和4年度の成果を深化させ、項書換えシステムの合流性を部分システムの合流性に還元する技法を開発、論文誌 LMCS 2022 において発表した。

Current Status of Research Progress
Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

自動証明において結合律・交換律を扱う基盤技術の研究を行い、当初の予定以上の成果を得た。一方で定理自動証明のための項索引の実装に想定以上の時間を要しており、全てが順調というわけではない。しかし概ねは順調に進展しているといえる。

Strategy for Future Research Activity

次年度は基本的に高階論理の自動演繹の研究に取り組むが、当該年度に得られた成果は萌芽的な成果が多く多分に改良の余地を残しているため、それら成果の深化も並行して行う。

Report

(2 results)
  • 2023 Research-status Report
  • 2022 Research-status Report
  • Research Products

    (11 results)

All 2024 2023 2022 Other

All Int'l Joint Research (1 results) Journal Article (1 results) (of which Peer Reviewed: 1 results,  Open Access: 1 results) Presentation (5 results) (of which Int'l Joint Research: 5 results) Remarks (4 results)

  • [Int'l Joint Research] インスブルック大学(オーストリア)

    • Related Report
      2023 Research-status Report
  • [Journal Article] Compositional Confluence Criteria2024

    • Author(s)
      Kiraku Shintani and Nao Hirokawa
    • Journal Title

      Logical Methods in Computer Science 20(1)

      Volume: 20(1)

    • Related Report
      2023 Research-status Report
    • Peer Reviewed / Open Access
  • [Presentation] Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs2024

    • Author(s)
      Nao Hirokawa, Dohan Kim, Kiraku Shintani, and Rene Thiemann
    • Organizer
      Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 147-161
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research
  • [Presentation] Hydra Battles and AC Termination2023

    • Author(s)
      Nao Hirokawa and Aart Middeldorp
    • Organizer
      Proceedings of the 8th International Conference on Formal Structures of Computation and Deduction, Leibniz International Proceedings in Informatics 260, pp. 12:10-12:16.
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research
  • [Presentation] Left-Linear Completion with AC Axioms2023

    • Author(s)
      Johannes Niederhauser, Nao Hirokawa, and Aart Middeldorp
    • Organizer
      Proceedings of the 29th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 14132, pp. 401-418
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research
  • [Presentation] Weighted Path Orders are Semantic Path Orders2023

    • Author(s)
      Teppei Saito and Nao Hirokawa
    • Organizer
      Proceedings of the 14th International Symposium on Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence, pp. 63-80.
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research
  • [Presentation] Compositional Confluence Criteria2022

    • Author(s)
      Kiraku Shintani and Nao Hirokawa
    • Organizer
      Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics, 2022.
    • Related Report
      2022 Research-status Report
    • Int'l Joint Research
  • [Remarks] 研究者ホームページ

    • URL

      http://www.jaist.ac.jp/~hirokawa/

    • Related Report
      2023 Research-status Report
  • [Remarks] 合流性ツール Hakusan

    • URL

      http://www.jaist.ac.jp/project/saigawa/

    • Related Report
      2023 Research-status Report
  • [Remarks] 合流性ツール Saigawa

    • URL

      https://www.jaist.ac.jp/project/saigawa/

    • Related Report
      2022 Research-status Report
  • [Remarks] 定理自動証明システム Toma

    • URL

      https://www.jaist.ac.jp/project/maxcomp/

    • Related Report
      2022 Research-status Report

URL: 

Published: 2022-04-19   Modified: 2024-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi