This package is built on the SMT solver Z3 to provide a programmatic semantics for a range of hyperintensional operators along with a general purpose methodology for developing novel programmatic semantic theories and studying their logics. You can find more information about the background theory here.

The Language of Thought

Rather than computing whether a given sentence is a logical consequence of some set of sentences by hand (typical in logic), these resources allow users to find countermodels or establish logical consequence up to a finite level complexity specified by the user. This package integrates with formal methods to provide tooling for quickly finding hyperintensional countermodels and establish validity in a propositional language with the following operators:

• neg for negation
• wedge for conjunction
• vee for disjunction
• rightarrow for the material conditional
• leftrightarrow for the material biconditional
• boxright for the must counterfactual conditional
• diamondright for the might counterfactual conditional
• Box for necessity
• Diamond for possibility
• Future read 'it will always be the case that'
• future read 'it will be the case that'
• Past read 'it always has been the case that'
• past read 'it has been the case that'
• leq for ground read 'sufficient for'
• sqsubseteq for essence read 'necessary for'
• equiv for propositional identity read 'just is for'
• preceq for relevance

More specific details about the implementation of this hyperintensional semantics can be found here.

TheoryLib

The model-checker includes a growing library of semantic theories, each of which:

• Introduces the primitives that make up a frame
• Defines the propositions over a frame
• Defines the models of the language by assigning sentence letters to propositions
• Provides semantic clauses for the operators included in the language
• Includes a range of examples of logical consequences and countermodels

Once the extension of a semantic theory has been adequately explored with adequate results, that theory can be included in the TheoryLib.

Licensing

ModelChecker is licensed under the GNU General Public License v3.0 (GPL-3.0). This license ensures that the software remains free and open-source. Key aspects of the licensing include:

• Core Package: The main ModelChecker framework is licensed under GPL-3.0
• Theory Library: All theories in the theory_lib directory are also individually licensed under GPL-3.0
• Derivative Works: According to GPL-3.0 terms, any derivative works, including new theories based on existing ones, must maintain the same license
• Academic Attribution: Each theory includes a CITATION.md file with proper academic attribution information

Contributing New Theories

When contributing a new theory to the ModelChecker framework:

1. Your contribution must be compatible with the GPL-3.0 license
2. Your theory will be automatically licensed under GPL-3.0 when added to the theory library
3. You retain copyright for your specific implementation but grant license under GPL-3.0
4. Academic attribution for your theory will be maintained in CITATION.md

The licensing structure is designed to ensure that the ModelChecker ecosystem remains open and accessible while providing proper attribution to theory authors.

Installation

Basic Installation

For core functionality (command line interface and model checking):

pip install model-checker

This installs the essential z3-solver dependency needed for constraint solving.

Optional Features

For Jupyter notebook integration with interactive visualizations:

pip install model-checker[jupyter]

For development tools (running tests):

pip install model-checker[dev]

For a complete installation with all features:

pip install model-checker[all]

More installation information can be found in the accessible instructions.

Updating

Once installed, you can check the current version of the model-checker with:

model-checker -v

To update to the latest version, run:

model-checker -u

Usage

Run model-checker in the terminal without arguments to create a new project with the following modules:

• semantic.py specifies the Z3 primitives, frame constraints, models, theory of logical consequence, defined semantic terms, theory of propositions, and print instructions for displaying countermodels for the default semantics.
• operators.py specifies the semantic clauses for the primitive operators included in the default language along with a number of defined operators.
• examples.py specifies the settings, a collection of examples, and the protocol for finding and printing countermodels if there are any.

Alternatively, run model-checker -l THEORY_NAME to create a copy of the semantic theory with the name 'THEORY_NAME'. The library of available semantic theories can be found here. Additional theories can be added by submitting a pull request.

After changing to the project directory that you created, run model-checker project_examples.py to find a countermodel if there is any. The example settings specify the following inputs where the defaults are indicated below:

• The number of atomic states to include in each model: N = 3.
• An option to require all sentence letters to be contingent: contingent = False.
• An option to require all sentence letters to have at least one verifier and at least one falsifier: non_empty = False.
• An option to prevent sentence letters from having the null state as a verifier or a falsifier: non_null = False.
• An option to prevent sentence letters from having overlapping verifiers or falsifiers: disjoint = False.
• The maximum time in seconds to spend looking for a model: max_time = 1.

A number of general settings may also be specified with the following:

• An option to print impossible states: print_impssible = False.
• An option to print all Z3 constraints or unsatisfiable core constraints: print_constraints = False.
• An option to print the Z3 model if there is any: print_z3 = False.
• An option to prompt the user to append the output to the current file or to create a new file: save_output = False.

Examples are specified by defining a list as follows:

# CF_CM_1: COUNTERFACTUAL ANTECEDENT STRENGTHENING

CF_CM_1_premises = ['(A \\boxright C)']
CF_CM_1_conclusions = ['((A \\wedge B) \\boxright C)']
CF_CM_1_settings = {
    'N' : 3,
    'contingent' : True,
    'non_null' : True,
    'non_empty' : True,
    'disjoint' : False,
    'max_time' : 1,
}

CF_CM_1_example = [
    CF_CM_1_premises,
    CF_CM_1_conclusions,
    CF_CM_1_settings,
]

The example CF_CM_1_example includes:

• A list of zero or more premises that are treated conjunctively: premises = [].
• A list of zero or more conclusions that are treated disjunctively: conclusions = [].
• A dictionary of settings where the defaults are indicated above.

Alternatively, users can define a general stock of example_settings, reusing these for an number of examples. Users can override these settings from the command line by including the following flags:

• Include -c to set contingent = True.
• Include -d to set disjoint = True.
• Include -e to set non_empty = True.
• Include -i to set print_impossibe = True.
• Include -n to set non_null = True.
• Include -p to set print_constraints = True.
• Include -s to set save_bool = True.
• Include -z to set print_z3 = True.

Additional flags have been included in order to manage the package version:

• Include -h to print help information about the package and its usage.
• Include -v to print the installed version number.
• Include -u to upgrade to the latest version.

Jupyter Notebook Integration

ModelChecker can be used interactively in Jupyter notebooks, allowing for dynamic exploration of logical models with an interactive interface.

Installation

To use ModelChecker in Jupyter notebooks, install with optional dependencies:

pip install ipywidgets matplotlib networkx

Basic Usage

For quick formula checking, both LaTeX and some unicode characters are accepted:

from model_checker.notebook import check_formula

# Check a counterfactual formula
check_formula("(A \\vee B \\boxright C) \\rightarrow (A \\boxright C)")

# Check a modal formula
check_formula("□(p → q) → (□p → □q)")

# Check with premises
check_formula("q", premises=["p", "p \\diamondright q"])

Interactive Explorer

For interactive exploration with a UI:

from model_checker.notebook import InteractiveModelExplorer

# Create and display the explorer
explorer = InteractiveModelExplorer()
explorer.display()

The interactive explorer provides:

• Formula input with syntax highlighting
• Theory selection and settings customization
• Multiple visualization options
• Ability to find alternative models

For a demonstration, see the examples/jupyter_demo.ipynb notebook and the examples/README_jupyter.md documentation.