A Case Study : Meyer's Formulation of a Specification and Theorem Proving with an SMT Solver Z3 (Model theoretic aspects of the notion of independence and dimension)

Abstract

An SMT solver is a program to solve satisfiability problems described in restricted first-order formulas. Recently, SMT solvers are becoming powerful and applied to solve concrete problems in many research areas. But a concrete problem requires a complex first-order formula, then the satisfiability of the resulting formula often cannot be solved with an SMT solver. In these cases, we must use some model-theoretic techniques (Skolemization, quantifier-elimination, etc.) to reduce the complexity of a given first-order formula. Our future goal is to propose a simple formal specification language and a validation method, which is based on a model-theoretic method, to fill a gap in natural languages and standard formal languages. In this paper, we show a case study. In the case study, we formalize a specification and its properties with Meyer s formulation, and then we prove some theorems for specifications with an SMT solver Z3.