Description and verification of national pension law in predicate logic, a case study using SMT solver z3py.

Abstract

A case study of checking correctness of the National Pension Law by formalizing it in predicate logic and applying automatic theorem proving tool Z3Py is described. Creation of laws has been done traditionally by hand, but in recent years a large number of laws and ordinances have been made, and in order to maintain their quality, it is considered effective to apply computer science, especially technologies cultivated with software engineering and artificial intelligence. In this paper, description of the national pension law in predicate logic and its verification by a SMT solver Z3Py are reported. We found that, despite the docu-ment level complexity of the law, its logical depth is not deep and such methods will be effective in making correct and errorless laws.