%0 Journal Article
%T Optimizing Compiler Schemas in RETE Network and their Formal Verification with PVS<br>RETE网络中的优化编译模式及其PVS形式验证
%A LIU Xiao-Jian CHEN Ping
%A <br>刘晓建
%A 陈平
%J 计算机科学
%D 2003
%I 
%X In the compilation of rule program to the intermediate code-RETE network, optimizing compilation is an important compiler schema,and is a necessary step in the compiler verification. In this paper,we discuss optimization schemas in rule program compilation, and prove the semantic equivalence theorems of these schemas. Firstly, the structure of RETE network and its PVS specification are represented. Secondly,three kinds of optimization schemas are listed. Then algorithms evaluating semantics of target RETE network are given. Finally,we prove the semantic e-quivalence theorems with theorem prover PVS (Prototype Verification System).
%K RETE network
%K Rule-based system
%K Compiler verification
%K Mechanized theorem proving
%K PVS<br>RETE网络
%K 优化编译模式
%K PVS
%K 形式验证
%K 编译器
%K 程序设计语言
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=8C3230981E5E1E1F&yid=D43C4A19B2EE3C0A&vid=340AC2BF8E7AB4FD&iid=B31275AF3241DB2D&sid=BBF7D98F9BEDEC74&eid=73579BC9CFB2D787&journal_id=1002-137X&journal_name=计算机科学&referenced_num=1&reference_num=11