AUTOMATED COMPOSITIONAL REASONING OF INTUITIONISTICALLY CLOSED REGULAR PROPERTIES
Yih-Kuen Tsay, Bow-Yaw Wang · International Journal of Foundations of Computer Science · 2009
Analysis of infinitary safety properties with automated compositional reasoning through learning is discussed in the paper. We consider the class of intuitionistically closed regular languages and show that it forms a Heyting algebra and is finitely approximatable. Subsequently, compositional proof rules can be verified automatically and learning algorithms for finitary regular languages suffice. We also establish an axiom to deduce circular compositional proof rules for the infinitary languages.