ModelChecker v1.0.0

The first stable release of ModelChecker - a programmatic semantics framework for computational logic powered by the Z3 SMT solver.

Key Features

• Automated countermodel discovery for invalid formulas across modal, counterfactual, and hyperintensional logics
• Four pre-built semantic theories: Logos (hyperintensional truthmaker semantics), Exclusion (unilateral semantics), Imposition (Fine's counterfactuals), and Bimodal (temporal-modal logic)
• Modular operator architecture supporting 19+ logical operators across extensional, modal, counterfactual, and constitutive subtheories
• Theory comparison tools for systematic exploration of logical principles
• Interactive Jupyter integration for exploratory semantic analysis
• Full Python API for building custom semantic theories

This release represents the first production-ready implementation of hyperintensional truthmaker semantics, enabling fine-grained reasoning about counterfactuals, grounding, and explanatory connections in computational logic.