Release v1.2.12

ModelChecker v1.2.12

Installation

pip install model-checker==1.2.12

What's Changed

See CHANGELOG.md for details.

Release v1.2.11

ModelChecker v1.2.11

Installation

pip install model-checker==1.2.11

What's Changed

See CHANGELOG.md for details.

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.

Bimodal Semantics

This release includes a bimodal intensional semantics in the theory_lib which can be used to create bimodal projects with:

model-checker -l bimodal

The hyperintensional semantics has also been extended to include an iterate setting which allows users to search for non-isomorphic models. Extensive documentation has also been included.

Modular Semantics

This release significantly refactors the code base to accommodate greater modularity for defining semantic clauses for different operators across different semantic theories. In addition to making it easy to add new operators with novel semantic clauses, this version makes it easy to compare define and compare different semantic theories. The CLI has been updated to generate new projects when run with no arguments so that users can easily adapt the default semantic theory which is used as a template. A number of definitions have also been exposed for easy importing.

Future patches will extend the utilities included for comparing theories and will add default unit tests to the project template so as to streamline implementation.

https://pypi.org/project/model-checker/

Finite Quantifiers, Contingency, and Optimization

Z3's quantifiers have been replaced by functions which generate finite conjunctions and disjunctions, leading to a massive performance gain. The following new features have also been included:

• The user can specify a max_time and is prompted to increase the time if the model-checker times out.
• The user can set an optimize variable with override flag -o to have the model-checker find a model with the smallest number of atomic elements within the max_time.
• The user can set the contingent variable with override flag -c to require all propositions to be contingent, i.e., to have some possible verifier and some possible falsifier. Since the null state cannot verify nor falsify a contingent proposition, constraints on propositions to only have non-null verifiers and falsifiers have been removed.

In addition to these features, the unit tests have been expanded to now include 120 examples which are divided by logical operators.

Interpreted propositions and disjunctive conclusions

This release provides more detailed printing and interprets conclusions disjunctively.