This package draws on the [Z3](https://github.com/Z3Prover/z3) SMT solver to provide a unified programmatic semantics and methodology for developing modular semantic theories and exploring their logics.
Rather than computing whether a given sentence is a logical consequence of some set of sentences by hand, these resources allow users to establish logical consequence over finite models, finding readable countermodels if there are any.
Whereas logic has traditionally focused on small language fragments, this project develops a unified semantics for the Logos, a language of thought for AI agents to plan and reason to promote transparent and verifiable reasoning that can be trusted.
In addition to the unified semantics for the Logos, this package provides support for users to develop their own programmatic semantic theories.
The [`TheoryLib`](src/model_checker/theory_lib/) includes the semantic theories that are available for users to import or use as a template to develop novel theories that can be contributed to the `TheoryLib` by pull request.
You can find more information about development [here](docs/DEVELOPMENT.md) and the background semantic theory provided for the Logos [here](http://www.benbrastmckie.com/research#access).
The semantics and logic for counterfactual conditionals is developed in this [paper](https://link.springer.com/article/10.1007/s10992-025-09793-8).
## Quick Start
### Installation
Basic installation with core functionality:
```bash
pip install model-checker
```
Installation with Jupyter support:
```bash
pip install model-checker[jupyter]
```
Development installation from source:
```bash
git clone https://github.com/benbrastmckie/ModelChecker
cd ModelChecker/Code
pip install -e .[dev]
```
### Command Line Usage
Create a new theory project:
```bash
model-checker
```
Create a project from existing theory:
```bash
model-checker -l logos
```
Check an example file:
```bash
model-checker examples/counterfactual_logic.py
```
### Python API Usage
```python
from model_checker.theory_lib import logos
from model_checker import BuildExample
# Get a theory
theory = logos.get_theory()
# Create and check a model
model = BuildExample("my_example", theory)
result = model.check_formula("\\Box p \\rightarrow p")
if result:
print("Formula is valid")
else:
print("Found countermodel:")
model.print_countermodel()
```
### Jupyter Notebook Usage
```python
from model_checker.jupyter import check_formula, ModelExplorer
# Quick formula check
check_formula("(p \\wedge q) \\equiv (q \\wedge p)")
# Interactive exploration
explorer = ModelExplorer()
explorer.display()
```
For comprehensive Jupyter integration documentation, see:
- [Jupyter Integration Guide](examples/README_jupyter.md)
- [Interactive Notebooks](src/model_checker/theory_lib/logos/notebooks/README.md)
- [Example Notebooks](notebooks/)
## Development
For complete development documentation, see:
- [Development Guide](docs/DEVELOPMENT.md) - Comprehensive development workflow
- [Architecture Documentation](ARCHITECTURE.md) - System design and patterns
- [Maintenance Standards](MAINTENANCE.md) - Coding and documentation guidelines
### Running Tests
Run all tests:
```bash
./run_tests.py
```
Run theory-specific tests:
```bash
./test_theories.py --theories logos exclusion
```
Run package component tests:
```bash
./test_package.py --components utils builder
```
For detailed testing documentation, see [Unit Tests Guide](../Docs/UNIT_TESTS.md).
### Creating a New Theory
Use the development CLI to create a new theory:
```bash
./dev_cli.py -l my_new_theory
```
This creates a complete theory template with:
- Semantic implementation skeleton
- Operator definitions
- Example formulas
- Test structure
- Documentation templates
For theory development guidance, see:
- [Theory Library Documentation](src/model_checker/theory_lib/README.md)
- [Theory Architecture Patterns](src/model_checker/theory_lib/README.md#theory-architecture-patterns)
### Development Tools
Debug an example with constraint printing:
```bash
./dev_cli.py -p -z examples/my_example.py
```
Launch Jupyter for interactive development:
```bash
./run_jupyter.sh
```
For advanced debugging and tools documentation, see [Tools Guide](../Docs/TOOLS.md).
## Package Architecture
ModelChecker follows a modular architecture with clear separation between:
1. **Core Framework** (`src/model_checker/`) - Base classes and interfaces
2. **Theory Library** (`src/model_checker/theory_lib/`) - Semantic theory implementations
3. **Utilities** (`src/model_checker/utils/`) - Helper functions and tools
4. **Jupyter Integration** (`src/model_checker/jupyter/`) - Interactive features
For detailed architecture documentation, see [ARCHITECTURE.md](ARCHITECTURE.md).
## Contributing
We welcome contributions! Please:
1. Read [MAINTENANCE.md](MAINTENANCE.md) for coding standards
2. Follow [STYLE_GUIDE.md](STYLE_GUIDE.md) for Python style
3. See [docs/DEVELOPMENT.md](docs/DEVELOPMENT.md) for workflow
4. Ensure all tests pass before submitting PRs
5. Include documentation for new features
## Related Documentation
- [Project Overview](../README.md) - Main project documentation
- [Installation Guide](../Docs/INSTALLATION.md) - Detailed installation instructions
- [Theory Library](src/model_checker/theory_lib/README.md) - Available theories
- [API Reference](src/model_checker/README.md) - Complete API documentation
- [Hyperintensional Semantics](../Docs/HYPERINTENSIONAL.md) - Theoretical background
Raw data
{
"_id": null,
"home_page": null,
"name": "model-checker",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.8",
"maintainer_email": null,
"keywords": "semantics, Z3, logic, counterfactuals, modality, model checker, theorem prover, hyperintensionality",
"author": null,
"author_email": "Benjamin Brast-McKie <benbrastmckie@gmail.com>, Miguel Buitrago <mbuit82@gmail.com>",
"download_url": "https://files.pythonhosted.org/packages/ca/b5/72bf5778d3a1b5abc46017b5e4079fb019472c7f08babee24478783161df/model_checker-0.9.31.tar.gz",
"platform": null,
"description": "This package draws on the [Z3](https://github.com/Z3Prover/z3) SMT solver to provide a unified programmatic semantics and methodology for developing modular semantic theories and exploring their logics.\nRather than computing whether a given sentence is a logical consequence of some set of sentences by hand, these resources allow users to establish logical consequence over finite models, finding readable countermodels if there are any.\nWhereas logic has traditionally focused on small language fragments, this project develops a unified semantics for the Logos, a language of thought for AI agents to plan and reason to promote transparent and verifiable reasoning that can be trusted.\n\nIn addition to the unified semantics for the Logos, this package provides support for users to develop their own programmatic semantic theories.\nThe [`TheoryLib`](src/model_checker/theory_lib/) includes the semantic theories that are available for users to import or use as a template to develop novel theories that can be contributed to the `TheoryLib` by pull request.\n\nYou can find more information about development [here](docs/DEVELOPMENT.md) and the background semantic theory provided for the Logos [here](http://www.benbrastmckie.com/research#access).\nThe semantics and logic for counterfactual conditionals is developed in this [paper](https://link.springer.com/article/10.1007/s10992-025-09793-8).\n\n## Quick Start\n\n### Installation\n\nBasic installation with core functionality:\n```bash\npip install model-checker\n```\n\nInstallation with Jupyter support:\n```bash\npip install model-checker[jupyter]\n```\n\nDevelopment installation from source:\n```bash\ngit clone https://github.com/benbrastmckie/ModelChecker\ncd ModelChecker/Code\npip install -e .[dev]\n```\n\n### Command Line Usage\n\nCreate a new theory project:\n```bash\nmodel-checker\n```\n\nCreate a project from existing theory:\n```bash\nmodel-checker -l logos\n```\n\nCheck an example file:\n```bash\nmodel-checker examples/counterfactual_logic.py\n```\n\n### Python API Usage\n\n```python\nfrom model_checker.theory_lib import logos\nfrom model_checker import BuildExample\n\n# Get a theory\ntheory = logos.get_theory()\n\n# Create and check a model\nmodel = BuildExample(\"my_example\", theory)\nresult = model.check_formula(\"\\\\Box p \\\\rightarrow p\")\n\nif result:\n print(\"Formula is valid\")\nelse:\n print(\"Found countermodel:\")\n model.print_countermodel()\n```\n\n### Jupyter Notebook Usage\n\n```python\nfrom model_checker.jupyter import check_formula, ModelExplorer\n\n# Quick formula check\ncheck_formula(\"(p \\\\wedge q) \\\\equiv (q \\\\wedge p)\")\n\n# Interactive exploration\nexplorer = ModelExplorer()\nexplorer.display()\n```\n\nFor comprehensive Jupyter integration documentation, see:\n- [Jupyter Integration Guide](examples/README_jupyter.md)\n- [Interactive Notebooks](src/model_checker/theory_lib/logos/notebooks/README.md)\n- [Example Notebooks](notebooks/)\n\n## Development\n\nFor complete development documentation, see:\n- [Development Guide](docs/DEVELOPMENT.md) - Comprehensive development workflow\n- [Architecture Documentation](ARCHITECTURE.md) - System design and patterns\n- [Maintenance Standards](MAINTENANCE.md) - Coding and documentation guidelines\n\n### Running Tests\n\nRun all tests:\n```bash\n./run_tests.py\n```\n\nRun theory-specific tests:\n```bash\n./test_theories.py --theories logos exclusion\n```\n\nRun package component tests:\n```bash\n./test_package.py --components utils builder\n```\n\nFor detailed testing documentation, see [Unit Tests Guide](../Docs/UNIT_TESTS.md).\n\n### Creating a New Theory\n\nUse the development CLI to create a new theory:\n```bash\n./dev_cli.py -l my_new_theory\n```\n\nThis creates a complete theory template with:\n- Semantic implementation skeleton\n- Operator definitions\n- Example formulas\n- Test structure\n- Documentation templates\n\nFor theory development guidance, see:\n- [Theory Library Documentation](src/model_checker/theory_lib/README.md)\n- [Theory Architecture Patterns](src/model_checker/theory_lib/README.md#theory-architecture-patterns)\n\n### Development Tools\n\nDebug an example with constraint printing:\n```bash\n./dev_cli.py -p -z examples/my_example.py\n```\n\nLaunch Jupyter for interactive development:\n```bash\n./run_jupyter.sh\n```\n\nFor advanced debugging and tools documentation, see [Tools Guide](../Docs/TOOLS.md).\n\n## Package Architecture\n\nModelChecker follows a modular architecture with clear separation between:\n\n1. **Core Framework** (`src/model_checker/`) - Base classes and interfaces\n2. **Theory Library** (`src/model_checker/theory_lib/`) - Semantic theory implementations\n3. **Utilities** (`src/model_checker/utils/`) - Helper functions and tools\n4. **Jupyter Integration** (`src/model_checker/jupyter/`) - Interactive features\n\nFor detailed architecture documentation, see [ARCHITECTURE.md](ARCHITECTURE.md).\n\n## Contributing\n\nWe welcome contributions! Please:\n\n1. Read [MAINTENANCE.md](MAINTENANCE.md) for coding standards\n2. Follow [STYLE_GUIDE.md](STYLE_GUIDE.md) for Python style\n3. See [docs/DEVELOPMENT.md](docs/DEVELOPMENT.md) for workflow\n4. Ensure all tests pass before submitting PRs\n5. Include documentation for new features\n\n## Related Documentation\n\n- [Project Overview](../README.md) - Main project documentation\n- [Installation Guide](../Docs/INSTALLATION.md) - Detailed installation instructions\n- [Theory Library](src/model_checker/theory_lib/README.md) - Available theories\n- [API Reference](src/model_checker/README.md) - Complete API documentation\n- [Hyperintensional Semantics](../Docs/HYPERINTENSIONAL.md) - Theoretical background\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "A hyperintensional theorem prover for modal, counterfactual conditional, constitutive explanatory, and extensional operators.",
"version": "0.9.31",
"project_urls": {
"Homepage": "https://github.com/benbrastmckie/ModelChecker",
"Issues": "https://github.com/benbrastmckie/ModelChecker/issues"
},
"split_keywords": [
"semantics",
" z3",
" logic",
" counterfactuals",
" modality",
" model checker",
" theorem prover",
" hyperintensionality"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "b84585a26e6cfd37aedd1f99ff571521a1c4ec11169cafd0894f961dcf70b9d7",
"md5": "6ad73b6dbf2ff35b97367d2208a73275",
"sha256": "27fe40d02e8657093a9f64d915d6608b7769cdc54ae00f64057a1df081e45ca4"
},
"downloads": -1,
"filename": "model_checker-0.9.31-py3-none-any.whl",
"has_sig": false,
"md5_digest": "6ad73b6dbf2ff35b97367d2208a73275",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.8",
"size": 1076347,
"upload_time": "2025-07-26T19:46:25",
"upload_time_iso_8601": "2025-07-26T19:46:25.651765Z",
"url": "https://files.pythonhosted.org/packages/b8/45/85a26e6cfd37aedd1f99ff571521a1c4ec11169cafd0894f961dcf70b9d7/model_checker-0.9.31-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "cab572bf5778d3a1b5abc46017b5e4079fb019472c7f08babee24478783161df",
"md5": "69cba92608d8bb94db7f1ac7c5d3b013",
"sha256": "9a0f7ae24563643e179df0d5f77b02d4d4614e19c8f2695843789807307dd885"
},
"downloads": -1,
"filename": "model_checker-0.9.31.tar.gz",
"has_sig": false,
"md5_digest": "69cba92608d8bb94db7f1ac7c5d3b013",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.8",
"size": 884026,
"upload_time": "2025-07-26T19:46:27",
"upload_time_iso_8601": "2025-07-26T19:46:27.459974Z",
"url": "https://files.pythonhosted.org/packages/ca/b5/72bf5778d3a1b5abc46017b5e4079fb019472c7f08babee24478783161df/model_checker-0.9.31.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2025-07-26 19:46:27",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "benbrastmckie",
"github_project": "ModelChecker",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"lcname": "model-checker"
}
JSON
