Research of Automated Deduction System for Linear Logic

LLPTTP(LLP Technology Theorem Prover)是经典逻辑子句形式的定理证明器(参考文献1)。该系统将给定的子句形式公式翻译成LLP线性逻辑程序设计语言程序，然后利用LLP编译系统进行编译和执行。评估表明，LLPTTP在处理TPTP问题集方面比PTTP(Prolog Technology Theorem Prover)和lolliCoP有更好的性能。该系统将给定的经典线性逻辑公式翻译成LLP线性逻辑程序设计语言程序，然后使用LLP编译系统编译/执行该程序。评估表明，LL2LLP在大多数基准问题上的性能优于其他线性逻辑定理证明工具，如LINRES、linseq和linTAP。该系统在验证系统中的应用与庆应大学的Okada教授共同完成了实时规范系统的验证研究。我们开发了一个基于线性逻辑的验证系统的原型，并在国际研讨会上展示了这一成果(参考文献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).