Research of Automated Deduction System for Linear Logic

在2002年至2005年期间完成了以下软件开发和研究。●LLPTTP（LLP Technology Theorem Prover）LLPTTP是经典逻辑子句形式的定理证明器（参考文献1）。该系统将给定的子句形式公式转换成LLP线性逻辑程序设计语言的程序，然后利用LLP编译系统编译/执行该程序.结果表明，LLPTTP对TPTP问题集的性能优于PTTP（Prolog Technology Theorem Prover）和lolliCoP.● LL 2LLP（Linear Logic to LLP）LL 2LLP是经典命题线性逻辑的定理证明器（参考文献2，6）.该系统将给定的经典线性逻辑公式转换成LLP线性逻辑程序设计语言的程序，然后使用LLP编译系统编译/执行该程序，测试结果表明，LL 2LLP在大多数基准问题上的性能优于其它线性逻辑定理证明器，如linres，linseq，●验证系统的应用与庆应义塾大学的冈田教授共同进行了实时规格系统的验证研究。我们开发了一个基于线性逻辑的验证系统原型，并在国际研讨会上展示了这一成果（参考文献4，5）。

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 systemJoint 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).