Optimizing Compiler Schemas in RETE Network and their Formal Verification with PVS
RETE网络中的优化编译模式及其PVS形式验证

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