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

Research of Automated Deduction System for Linear Logic

Research Project

Project/Area Number 14580375
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field 計算機科学
Research InstitutionKobe University

Principal Investigator

TAMURA Naoyuki  Kobe University, Information Science and Technology Center, Professor, 学術情報基盤センター, 教授 (60207248)

Co-Investigator(Kenkyū-buntansha) BANBARA Mutsunori  Kobe University, Information Science and Technology Center, Lecturer, 学術情報基盤センター, 講師 (80290774)
Project Period (FY) 2002 – 2004
Project Status Completed (Fiscal Year 2004)
Budget Amount *help
¥4,000,000 (Direct Cost: ¥4,000,000)
Fiscal Year 2004: ¥1,300,000 (Direct Cost: ¥1,300,000)
Fiscal Year 2003: ¥1,300,000 (Direct Cost: ¥1,300,000)
Fiscal Year 2002: ¥1,400,000 (Direct Cost: ¥1,400,000)
KeywordsLinear Logic / Automated Deduction / Automated Reasoning / Theorem Proving
Research Abstract

The following software development and research have been done during 2002〜2005 years.
●LLPTTP (LLP Technology Theorem Prover)
LLPTTP is a theorem prover for clausal forms of classical logic (REFERENCE 1). This system translates a given clausal form formula into a program of LLP Linear Logic Programming Language, then compiles/executes the program by using the LLP compiler system.
The evaluation shows LLPTTP has a better performance for TPTP problem set compared with PTTP (Prolog Technology Theorem Prover) and lolliCoP.
●LL2LLP (Linear Logic to LLP)
LL2LLP is a theorem prover for classical propositional linear logic (REFERENCE 2,6). This system translates a given classical linear logic formula into a program of LLP Linear Logic Programming Language, then compiles/executes the program by using the LLP compiler system.
The evaluation shows LL2LLP has a much better performance for most of the benchmark problems compared with other linear logic theorem provers, such as linres, linseq, and linTAP.
●Application to a verification system
Joint research on a verification of a real-time specification system has been done with Prof. Okada of Keio University. We developed a prototype of the verification system based on linear logic, and presented/demonstrated the accomplishment at international workshops (REFERENCE 4,5).

Report

(4 results)
  • 2004 Annual Research Report   Final Research Report Summary
  • 2003 Annual Research Report
  • 2002 Annual Research Report
  • Research Products

    (22 results)

All 2005 2004 2003 2002 Other

All Journal Article (15 results) Book (1 results) Publications (6 results)

  • [Journal Article] 線形論理型言語コンパイラ処理系を用いた古典命題線形論理の定理証明システム2005

    • Author(s)
      田村直之, 番原睦則
    • Journal Title

      コンピュータソフトウェア 22・1

      Pages: 98-103

    • NAID

      130005006638

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Annual Research Report 2004 Final Research Report Summary
  • [Journal Article] Classical propositional linear logic theorem prover on a linear logic programming language compiler system2005

    • Author(s)
      N.Tamura, M.Banbara
    • Journal Title

      A Proof Theory Workshop, Keio University

    • NAID

      130005006638

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Classical Propositional Linear Logic Theorem Prover on a Linear Logic Programming Language Compiler System2005

    • Author(s)
      N.Tamura, M.Banbara
    • Journal Title

      Computer Software 22-1

      Pages: 98-103

    • NAID

      130005006638

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Classical propositional linear logic theorem prover on a linear logic programming language compiler system2005

    • Author(s)
      N.Tamura, M.Banbara
    • Journal Title

      A Proof Theory Workshop(Keio University)

    • NAID

      130005006638

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Demonstration of Unsafe Time Condition Extraction for Train-Gate Controller2004

    • Author(s)
      N.Tamura, M.Banbara他
    • Journal Title

      Workshop on Proof Theory and its Applications, Keio University

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Demonstration of Unsafe Time Condition Extraction for Train-Gate Controller2004

    • Author(s)
      N.Tamura, M.Banbara, et al.
    • Journal Title

      Workshop on Proof Theory and its Applications(Keio University)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] 線形論理型言語コンパイラ処理系を用いた古典命題線形論理の定理証明システム2004

    • Author(s)
      田村直之, 番原睦則
    • Journal Title

      日本ソフトウェア科学会第20回全国大会

    • NAID

      130005006638

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Demonstration of Unsafe Time Condition Extraction for Train-Gate Controller2004

    • Author(s)
      N.Tamura, M.Banbara他
    • Journal Title

      Proof Theory and its Applicationsに関する合同セミナー

    • Related Report
      2004 Annual Research Report
  • [Journal Article] LLPTTP:線形論理型言語コンパイラ処理系を用いた定理証明システム2003

    • Author(s)
      田村直之, 番原睦則
    • Journal Title

      コンピュータソフトウェア 20・5

      Pages: 90-96

    • NAID

      130006949877

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Demonstration of Compiler Systems for Linear Logic Programming Languages and their Applications2003

    • Author(s)
      M.Banbara, T.Tanizawa, N.Tamura
    • Journal Title

      Workshop on Logic and Computation, Keio University

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] LLPTTP : Theorem Prover using Compiler of a Linear Logic Programming Language2003

    • Author(s)
      N.Tamura, M.Banbara
    • Journal Title

      Computer Software 20-5

      Pages: 90-96

    • NAID

      130004548997

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Demonstration of Compiler Systems for Linear Logic Programming Languages and their Applications2003

    • Author(s)
      M.Banbara, T.Tanizawa, N.Tamura
    • Journal Title

      Workshop on Logic and Computation(Keio University)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] [特別招待論文]線形論理と論理プログラミング2002

    • Author(s)
      田村直之
    • Journal Title

      電子情報通信学会技術研究報告 102・91

      Pages: 37-42

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Linear Logic and Logic Programming [Special Invited Paper]2002

    • Author(s)
      N.Tamura
    • Journal Title

      Technical Report of the Institute of Electronics, Information and Communication Engineers 102-91

      Pages: 37-42

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Journal Article] Design and Implementation of Linear Logic Programming Languages2002

    • Author(s)
      M.Banbara
    • Journal Title

      Ph.D Dissertation(Graduate School of Science and Technology, Kobe University)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Book] Design and Implementation of Linear Logic Programming Languages2002

    • Author(s)
      M.Banbara
    • Total Pages
      97
    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2004 Final Research Report Summary
  • [Publications] 田村直之: "LLPTTP:線形論理型言語コンパイラ処理系を用いた定理証明システム"コンピュータソフトウェア. 20・5. 90-96 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] S.Ohnishi: "Efficient Representation of Discrete Sets for Constraint Programming"Lecture Notes in Computer Science 2833 : Proc.9th Int'l Conf.on Principles and Practice of Constraint Programming. 920-924 (2003)

    • Related Report
      2003 Annual Research Report
  • [Publications] M.Banbara, T.Tanizawa, N.Tamura: "Demonstration of Compiler Systems for Linear Logic Programming Languages and their Applications"Workshop on Logic and Computation with the Special Intensive Lecture Series by J-Y. Girard. (口頭発表). (2003)

    • Related Report
      2002 Annual Research Report
  • [Publications] 田村直之, 番原睦則: "LLPTTP:線形論理型言語コンパイラ処理系を用いた定理証明システム"日本ソフトウェア科学会第19回大会講演論文集. 7A-4 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] 田村直之: "[特別招待論文]線形論理と論理プログラミング"電子情報通信学会技術研究報告. 102・91. 37-42 (2002)

    • Related Report
      2002 Annual Research Report
  • [Publications] M.Banbara: "Design and Implementation of Linear Logic Programming Languages"神戸大学大学院自然科学研究科 学位論文. 97 (2002)

    • Related Report
      2002 Annual Research Report

URL: 

Published: 2002-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi