SAT vs. SMV for automatic validation of tabular property of superintuitionistic logics

This paper considers theoretical background and experimental compar- ison of two approaches to automatic recognition of tabular property of superintu- itionistic logics. A principle opportunity for automatization is based on theoretical results of L.L. Maksimova that were obtained in 1973{2003 and their algorithmic interpretation that was developed recently by P.A. Schreiner. The experimental approaches under study are: (1) Computation Tree Logic (CTL) symbolic model checking, and (2) Boolean satisfiability (SAT) decision procedure. Efficiency of SAT-based approach to tabularity is demonstrated by a number of experiments.