Skip to content
BranchesTags

Repository files navigation

ModelChecker: Unified Programmatic Semantics Framework

Code → | Documentation → | Theory Library →

Overview

The ModelChecker provides a programmatic framework for developing and exploring modular semantic theories. Built on the SMT solver Z3, it enables researchers to establish logical consequence over finite models, automatically generating readable countermodels when formulas or inferences are invalid.

This talk at the Topos Institute provides an overview of the project.

Installation

Basic Installation

pip install model-checker

Requires Python 3.10 or later.

With Jupyter Support

pip install model-checker[jupyter]

For Jupyter notebook features and interactive exploration, see the Jupyter Integration Guide.

With the cvc5 Solver Backend

Z3 is the default solver. The optional cvc5 backend is a separate package:

pip install cvc5

Select a backend at run time with --z3 (default) or --cvc5.

Development Installation

git clone https://github.com/benbrastmckie/ModelChecker
cd ModelChecker/code
# Use the development CLI to run locally without installation:
./dev_cli.py src/model_checker/theory_lib/logos/examples.py

For comprehensive development setup instructions, including virtual environments and platform-specific guidance, see the Developer Setup Guide. NixOS users can use the provided flake.nix configuration (nix develop at the repository root) for automatic environment setup.

Installation Guides

For comprehensive installation instructions including platform-specific guides, virtual environments, and troubleshooting, see the Installation Documentation.

Quick Links:

Quick Start

1. Create a Project

# Create a copy of the logos semantics (default)
model-checker

# Or load a specific theory
model-checker -l logos        # Hyperintensional semantics with all subtheories
model-checker -l exclusion    # Unilateral exclusion semantics
model-checker -l imposition   # Fine's counterfactual semantics
model-checker -l bimodal      # Bimodal logic for tense and circumstantial modalities

This creates a project directory with examples.py, a semantic/ package, operators.py, iterate.py, subtheories/, tests, and docs. To load only some of the logos subtheories, pass them to get_theory in your examples.py:

from model_checker.theory_lib import logos

theory = logos.get_theory(subtheories=['extensional', 'counterfactual'])

2. Run Examples

# Run the examples file created in your project
model-checker examples.py

# Compare multiple theories
model-checker examples.py --maximize

# Save results in various formats
model-checker examples.py --save           # Both formats (markdown and json)
model-checker examples.py --save json      # JSON only

3. Next Steps

The ModelChecker Methodology

The ModelChecker provides a systematic methodology for developing and studying semantic theories. This section provides an overview of the workflow. For the complete methodology guide, see docs/usage/WORKFLOW.md.

1. Create Your Theory Project

Start by creating a new project or loading an existing theory:

# Create a copy of the logos semantics
model-checker                                        # Creates a logos semantics by default with all subtheories

# Load an existing theory as starting point
model-checker -l logos                               # Hyperintensional truthmaker semantics
model-checker -l exclusion                           # Unilateral exclusion semantics
model-checker -l imposition                          # Fine's counterfactual semantics
model-checker -l bimodal                             # Bimodal logic for tense and circumstantial modalities

This creates a complete project directory with examples.py, a semantic/ package, operators.py, iterate.py, and supporting files. See Project Creation Guide for detailed instructions.

2. Develop Examples

Edit the examples.py file to test logical inferences relevant to your theory:

# Run your examples
model-checker examples.py

Define a range of examples in order to evaluate their behavior in your theory. See the Examples Guide and Settings Guide for details.

3. Adapt Semantic Framework

Modify the semantic/ package to implement your specific semantic theory. Add new constraints, modify existing ones, or create entirely new semantic frameworks to capture the logical principles that distinguish your theory. See the Semantics Guide.

4. Define Custom Operators

Extend your theory's expressive power with new operators:

  • Defined operators in operators.py - shortcuts for combinations of existing operators
  • Primitive operators requiring semantic interpretation in the semantic/ package

See the Operators Guide for implementation patterns.

5. Iterate Models and Compare Theories

Explore the space of models your theory allows and systematically compare with alternative approaches:

# Test single theory
model-checker examples.py

# Compare multiple theories
model-checker examples.py --maximize

# Run the same examples against the cvc5 backend instead of Z3
model-checker examples.py --cvc5

See the Tools Guide for model iteration and theory comparison.

6. Save and Export Results

Export your findings in formats suitable for analysis or publication:

model-checker examples.py --save           # Both formats (markdown and json)
model-checker examples.py --save json      # Machine-readable JSON
model-checker examples.py --save markdown  # Human-readable markdown

See the Output Guide for format options.

Complete Methodology

This systematic approach enables you to:

  1. Start with working theories as foundations
  2. Test logical inferences computationally
  3. Customize semantic behavior through constraints
  4. Extend expressive power with new operators
  5. Explore the space of possible models
  6. Compare different theoretical approaches
  7. Document and share your findings

For the complete step-by-step methodology with detailed examples and advanced techniques, see the full Methodology Guide.

Project Structure

ModelChecker/
├── code/                           # Main implementation directory
│   ├── src/                        # Source code (the `model_checker` package)
│   ├── docs/                       # Technical documentation
│   ├── scripts/                    # Development and maintenance scripts
│   └── tests/                      # Test suites
├── docs/                           # General project documentation
│   ├── installation/               # Installation guides
│   ├── usage/                      # Practical usage guides
│   │   ├── PROJECT.md              # Project creation
│   │   ├── EXAMPLES.md             # Writing examples
│   │   ├── SETTINGS.md             # Configuration settings
│   │   ├── SEMANTICS.md            # Semantic constraints
│   │   ├── OPERATORS.md            # Defining operators
│   │   ├── TOOLS.md                # Advanced tools
│   │   ├── OUTPUT.md               # Saving results
│   │   └── WORKFLOW.md             # Complete methodology
│   ├── architecture/               # System architecture
│   └── theory/                     # Theoretical background
├── oracle/                         # Standalone differential-oracle tree (not shipped in the wheel)
├── latex/                          # Paper sources
├── talks/                          # Slides and talk materials
├── images/                         # Screenshots and diagrams
├── flake.nix                       # Nix development environment
└── README.md                       # This file

Main Directories

code/ - Main implementation directory containing the ModelChecker package source code, development tools, and technical documentation. Includes the core framework, theory library implementations, builder system, iteration engine, and comprehensive test suites. This is where developers work on extending the framework and contributing new theories. See code/README.md for package documentation.

docs/ - Project-level documentation for understanding the ModelChecker's theoretical foundations, development architecture, and advanced usage. Contains guides for installation, development workflows, research architecture, and detailed explanations of the Z3-based implementation approach. Essential reading for researchers and contributors. See docs/README.md for documentation navigation.

oracle/ - Standalone differential-oracle tree used to cross-check the semantics against independently written reference implementations. It is excluded from the published wheel and is not needed to use the package.

images/ - Visual documentation including architecture diagrams, countermodel visualizations, and screenshots demonstrating the framework in action. Helps illustrate complex semantic concepts and usage patterns that are difficult to convey through text alone.

Documentation

For New Users

For Researchers

For Developers

Key Features

1. Modular Semantic Theories

  • Hyperintensional Bilateral Semantics (Logos): 18 operators across 4 subtheories
  • Unilateral Exclusion Semantics (4 operators): Solving the False Premise Problem
  • Fine's Counterfactual Semantics (13 operators): Imposition semantics for counterfactuals
  • Bimodal Logic (17 operators): Intensional semantics for reasoning with both tense and modal operators

2. Computational Tools

  • Z3 SMT Integration: Automated model finding and constraint solving
  • Dual Solver Backends: Z3 by default, with optional cvc5
  • Countermodel Visualization: Understand why formulas fail
  • Model Iteration: Find multiple non-isomorphic models satisfying constraints
  • Semantic Comparison: Run multiple semantic theories on the same examples

3. Development Framework

  • Theory Templates: Quickly create new semantic theories
  • Modular Architecture: Compose operators with automatic dependencies
  • Comprehensive Testing: Unit tests, integration tests, and example validation
  • Rich Documentation: From API references to theoretical guides

Theory Highlights

Logos: Hyperintensional Truthmaker Semantics

  • 18 operators across 4 modular subtheories (extensional, modal, constitutive, counterfactual)
  • Sensitive to differences in subject-matter via verifier/falsifier sets
  • Distinguishes necessarily equivalent propositions
  • Supports modal, counterfactual, constitutive, and relevance reasoning

Exclusion: Unilateral Semantics

  • Implements Bernard & Champollion's exclusion operator in a unilateral semantic
  • Uses witness predicates for proper negation handling

Imposition: Fine's Counterfactual Theory

  • Evaluates counterfactuals via imposition
  • Uses primitive imposition relation on states

Bimodal: Temporal-Modal Logic

  • Facilitates reasoning about time and possibility
  • World histories as functions from times to world states
  • Includes past, future, and modal operators

Contributing

We welcome contributions! Please:

  1. Follow the Development Guide for workflow
  2. Use the standard examples.py structure for examples
  3. Ensure all tests pass before submitting PRs — run ./run_tests.py from code/, or PYTHONPATH=src pytest tests/ -v for pytest directly
  4. Include documentation for new features
  5. Read code/docs/core/CODE_STANDARDS.md for standards

Academic References

Citing the Software

Brast-McKie, B. (2025). Model-Checker: A Programmatic Semantics Framework. https://github.com/benbrastmckie/ModelChecker

Primary Sources

License

This project is licensed under GPL-3.0. See code/LICENSE for details.

Support

If you find ModelChecker useful, please consider starring the repository to help others discover it. To receive notifications about new releases:

  1. Click "Watch" on the GitHub repository
  2. Select "Custom" → "Releases" to be notified only about new versions

We encourage users to report bugs and suggest features by creating issues. When creating an issue, please:

  • Check existing issues to avoid duplicates

  • Provide minimal reproducible examples for bugs

  • See troubleshooting guide for common problems

  • Issues: GitHub Issues

  • Contact: See repository for contact information

Code → | Documentation → | Getting Started →

About

A hyperintensional theorem prover for rapidly prototyping modular semantic theories

pypi.org/project/model-checker/

Topics

counterfactualshyperintensionalitysemanticsz3-smt-solver

Resources

Readme
Activity

Stars

13 stars

Watchers

5 watching

Forks

3 forks
Report repository

Releases

Packages

Used by

Contributors

Languages