Automated Proofs of Horn-Clause Inductive Theorems for Conditional Term Rewriting Systems.

• KURITA Taichi

  Graduate School of Science and Technology, Niigata University

• AOTO Takahito

  Institute of Science and Technology, Niigata University

Bibliographic Information

Other Title

• 条件付き項書き換えシステムにおけるホーン節帰納的定理の自動証明
• ジョウケン ツキ コウ カキカエ システム ニ オケル ホーンセツ キノウテキ テイリ ノ ジドウ ショウメイ

Abstract

Inductive validity is an important characterization of term rewriting systems (TRSs). The notion of inductive validity is also adapted in conditional term rewriting systems (CTRSs). Rewriting induction is a method for proving inductive validity of TRSs originally intended for proving equational conjectures. In this paper, we propose an automated method to prove inductive validity of Horn-clauses (conditional equations) of deterministic oriented CTRSs of type 3. We first show how to deal with proving inductive validity of CTRSs via unraveling transformation from oriented CTRSs to TRSs, and reveal the class of CTRSs for which this approach works. Then, we give an extension of rewriting induction to deal with Horn-clause conjectures, and prove the correctness of the proposed method. We also report on an implementation of the automated inductive theorem prover based on the proposed method, and a preliminary experiment to evaluate the effectiveness of our approach.

Journal

• Computer Software

  Computer Software 36 (2), 2_61-2_75, 2019-04-26

  Japan Society for Software Science and Technology

Details

• CRID: 1390845713077904128
• NII Article ID: 130007666999
• NII Article ID: 40021922633
• NII Book ID: AN10075819
• DOI: 10.11309/jssst.36.2_61
• NDL BIB ID: 029751072
• ISSN: 02896540
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I029751072
• Text Lang: ja
• Data Source:
  • JaLC
  • NDL
  • CiNii Articles
  • KAKEN
• Abstract License Flag: Disallowed