ET-BASED BIDIRECTIONAL SEARCH FOR PROVING FORMULAS IN THE CLASS ES

In this paper, we propose a new method for proving the correctness of Logical Equivalences (LEs) in a newly defined class called ES. Proving the correctness of LEs is important for guaranteeing the correctness of Equivalent Transformation (ET) rules made from LEs. ET rules are useful for constructing correct sequential and parallel programs. The proposed method proves the equivalence of the declarative meaning of two definite clause sets using a bidirectional search that starts from two different points simultaneously. In the proposed method, the two definite clause sets at the starting points are transformed by ET rules. The method can generate ET rules that are essential for advancing the proof along with the general unfolding rules that are given before computing the proof. Class ES is a superclass of the classes proposed in past studies and therefore covers the LEs they contain