VMDV: A 3D Visualization Tool for Modeling, Demonstration, and Verification

In the setting of automated theorem proving, the output of an automated theorem prover is usually presented in text format, which is often too heavy to be understood. In the setting of model checking, it would be helpful if one can observe, at the same time, both the model structure under consideration and the verification procedure. To address these problems, a 3D visualization tool for modeling, demonstration and verification (VMDV for short) is proposed in this paper. The facilities of VMDV are illustrated by applying it to an automated theorem prover.