A hyperintensional model checker for counterfactual conditionals
Project description
Model Checker
This project draws on the Z3 theorem prover to provide tools for proving theorems and finding countermodels for counterfactual conditional and modal claims.
Installation
Install Python 3 and run the following commands in the terminal:
pip install model-checker
The project has the z3-solver
as a dependency.
Detailed installation instructions are provided in the GitHub repository.
Instructions
To generate a test file run model-checker
without arguments.
Alternatively, run model-checker path/to/test_file.py
if the test_file.py
already exists.
A number of examples are provided in the GitHub repository.
Each file must specify a set of premises
and conclusions
which are treated conjunctively, and the number N
of atomic states to include in each model.
Optionally, the user can specify whether to print the Z3 constraints when a model is found, or the unsatisfiable core when no model exists, as well as an option to save the output.
Semantics
The semantics included is hyperintensional insofar as sentences are evaluated at states which may be partial rather than total as in intensional semantic theories.
States are modeled by bitvectors (e.g., #b00101
) of a specified length, where state fusion is modeled by the bitwise OR operator |
.
States are named by lowercase letters for the sake of printing readable countermodels.
More information can be found in the GitHub repository. The hyperintensional semantic theory for counterfactual conditionals is motivated and elaborated in this draft. For the background hyperintensional theory of propositions, see this paper.
Syntax
The language currently includes operators for the counterfactual conditional boxright
, modal operators for necessity Box
and possibility Diamond
, and the extensional operators for conjunction wedge
, disjunction vee
, material conditional rightarrow
, material biconditional leftrightarrow
, and negation neg
.
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for model_checker-0.2.17-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 4597e69e637711cad71e7ae146fe4d512df260b74801d7c657df42a622437992 |
|
MD5 | f074ccd3b9991b9154bbf3cce3e8788b |
|
BLAKE2b-256 | 044484f13fa24367326f5bd2190d6e4d6562f727775569a7ad1d70d18a8388e4 |