GENERATION OF LOGICAL EQUIVALENCES BELONGING TO THE C2LE CLASS APPLIED TO PROGRAM SYNTHESIS BASED ON EQUIVALENT TRANSFORMATION

摘要

This paper proposes a framework that automatically generates multiple logical equivalences belonging to the C2LE class from a goal clause. A logical equivalence is a mathematical formula that describes the equivalence of the declarative meaning between two sets of atomic formulas, and is used to generate programs based on equivalent transformation. In the C2LE class, all atomic formulas are mutually connected via variables. The proposed framework consists of two functions, a generator and a filter, newly defined in this paper. The generator first acquires multiple pairs of sets consisting of atomic formulas from a goal clause, and then generates multiple logical equivalences from the obtained pairs by simple formula transformation. The filter uses an instantiation check to remove incorrect logical equivalences that do not specify equivalence between two sets of atomic formulas. An instantiation check is an original method to determine if two definite clauses are equivalent by specializing the targeted clauses. Experimental results indicate that the proposed framework works efficiently to generate logical equivalences that are useful to generate correct and efficient programs. Furthermore, we also show that the proposed framework can generate logical equivalences that cannot be generated using extant frameworks.