ModalLens

Project information

ModalLens is a research prototype for exploring and refining modal theories. The upcoming release will combine three layers: formal evidence, structural and learned analysis, and natural-language explanation.

Using Isabelle/HOL and Nitpick, it enumerates finite models and countermodels through blocking axioms, while Leo-III contributes proof evidence via TPTP/THF. The models are visualized as graphs and analysed using structural features, graphlets, clustering, and learned representations of heterogeneous semantic graphs to identify recurring patterns and differences between model families.

Selected structural patterns can then be translated into candidate refinement axioms that exclude the corresponding configurations. These axioms can be adopted automatically or with user input, followed by renewed model enumeration and analysis to examine the effects of each refinement.

LLM-generated explanations draw on the formal and structural evidence to explain findings and proposed refinements. Recorded provenance, reproducible runs, and visual exports make the process inspectable and suitable for experimental evaluation.

specification