| Name | mvmt JSON |
| Version |
0.0.9
JSON |
| download |
| home_page | |
| Summary | A package for checking the validity of many-valued modal formulas |
| upload_time | 2023-10-06 10:20:00 |
| maintainer | |
| docs_url | None |
| author | |
| requires_python | >=3.8 |
| license | |
| keywords |
logic
modal logic
tableau
|
| VCS |
 |
| bugtrack_url |
|
| requirements |
No requirements were recorded.
|
| Travis-CI |
No Travis.
|
| coveralls test coverage |
No coveralls.
|
# Many-Valued Modal Tableau (mvmt)
## Description
This repo contains the implementation of a desicion procedure for checking the validity of many-valued modal logic formulas. It is based on expansions of Fitting's work in [[1]](#1) and [[2]](#2). The proof of the correctness and termination of the procedure forms part of my master's dissertation which is in progress and will be linked after it has been submitted.
## Installation
```bash
pip install mvmt
```
## Getting Started
If you just want to use the package,
`pip install mvmt` and use the modules provided. See the colab notebook for example usages.
<a target="_blank" href="https://colab.research.google.com/github/WeAreDevo/Many-Valued-Modal-Tableau/blob/main/mvmt_demo.ipynb">
<img src="https://colab.research.google.com/assets/colab-badge.svg" alt="Open Demo In Colab"/>
</a>
If you would like to edit and run the source code directly, see the [For Developers](#for-developers) section.
## Function Documentation
This section describes the useful functions provided by the package.
### `utils.construct_heyting_algebra`
#### Description
A useful wrapper function for creating a `algebra.HeytingAlgebra` object from a user supplied `json` specification of a Heyting algebra. See below for the convention used to specify algebras in a `json` form.
#### Parameters
- `file_path` (`str`, optional): File path to `json` file containing a specification of a Heyting algebra.
- `python_dict` (`dict`, optional): Python `dict` giving the `json` specification of a Heyting algebra. Default is `None`.
At least one of the arguments must be given. The specification should have the following format:
```
{
"elements": ["<t1>","<t2>",...,"<tn>"],
"order": {"<t1>": ["<t1_1>",...,"<t1_k1>"], "<t2>": ["<t2_1>",...,"<t2_k2>"],...,"<tn>": ["<tn_1>",...,"<tn_kn">]},
"meet": {
"<t1>": {"<t1>": "<m1_1>", "<t2>": "<m1_2>", ..., "<tn>": "<m1_n>"},
"<t2>": {"<t1>": "<m2_1>", "<t2>": "<m2_2>", ..., "<tn>": "<m2_n>"},
.
.
.
"<tn>": {"<t1>": "<mn_1>", "<t2>": "<mn_2>", ..., "<tn>": "<mn_n>"},
},
"join": {
"<t1>": {"<t1>": "<j1_1>", "<t2>": "<j1_2>", ..., "<tn>": "<j1_n>"},
"<t2>": {"<t1>": "<j2_1>", "<t2>": "<j2_2>", ..., "<tn>": "<j2_n>"},
.
.
.
"<tn>": {"<t1>": "<jn_1>", "<t2>": "<jn_2>", ..., "<tn>": "<jn_n>"},
}
}
```
Where each angle bracket string in the above should be replaced with a string denoting a truth value. Such a string must match the regex `[a-o0-9]\d*`. That is, it should be a string of decimal digits, or a letter between a and o (inclusive) followed by a string of decimal digits.
If we assume the json is intended to represent a heyting algebra $\mathcal{H}=(H,\land,\lor,0,1, \leq)$, and $I$ is the mapping from the strings denoting truth values to the actual truth values in $H$, then the json should be interpreted as follows:
- $a \in H$ iff $a=I$("<ti>") for some `"<ti>"` in `elements`.
- `"<ti>"` is in `order["<tk>"]` iff $I$("<tk>") $\leq I$("<ti>")
- `meet["<ti>"]["<tk>"]=="<mi_k>"` iff $I$("<mi_k>") $= I$("<ti>") $\land I$("<tk>")
- `join["<ti>"]["<tk>"]=="<ji_k>"` iff $I$("<ji_k>") $= I$("<ti>") $\lor I$("<tk>")
For example, a specification of the three-valued Heyting algebra $(\{0,\frac{1}{2},1\}, \land, \lor, 0,1,\leq)$ with $I(\texttt{"0"})=0, I(\texttt{"a"})=\frac{1}{2}, I(\texttt{"1"})=1$ is given by:
```json
{
"elements": ["0","a","1"],
"order": {
"0": ["0","a","1"],
"a": ["a","1"],
"1": ["1"]
},
"meet": {
"0": {"0": "0","a": "0","1": "0"},
"a": {"0": "0","a": "a","1": "a"},
"1": {"0": "0","a": "a","1": "1"}
},
"join": {
"0": {"0": "0","a": "a","1": "1"},
"a": {"0": "a","a": "a","1": "1"},
"1": {"0": "1","a": "1","1": "1"}
}
}
```
#### Note:
Only **one** of the `order`, `meet` or `join` fields needs to be specified and the other two can be left out of the `json`. If at least one of these is specified, the others can be uniquely determined. See the example code.
#### Returns
(`algebra.HeytingAlgebra`) A `algebra.HeytingAlgebra` object storing the algebra represented by the inputed specification.
#### Example
```python
from mvmt import algebra, utils
# Specification of a four-valued Heyting algebra
spec = {
"elements": ["0","a","b","1"],
"order": {
"0": ["0","a","b","1"],
"a": ["a","1"],
"b": ["b","1"],
"1": ["1"]}
}
# Example usage
H: algebra.HeytingAlgebra = utils.construct_heyting_algebra(python_dict=spec)
print(H.meet(algebra.TruthValue("a"),algebra.TruthValue("b")))
```
```plaintext
# Output
0
```
### `syntax.parse_expression`
#### Description
Produces the syntax parse tree of a modal formula.
#### Parameters
- `expression` (`str`, required): A modal formula.
`expression` must belong to the language generated by the grammar
```
expression ::= expression & expression
| expression | expression
| expression -> expression
| [] expression
| <> expression
| (expression)
| VAR
| VALUE
```
`VAR` is a terminal symbol matching the regex `[p-z]\d*`, denoting a propositional variable.
`VALUE` is a terminal symbol matching the regex `[a-o0-9]\d*`. It denotes a truth value from the algebra, and as such it must be the same as one of the strings given in `elements` of the algebra specification.
#### Returns
(`syntax.AST_Node`) The root node of the parse tree.
#### Example
```python
from mvmt import syntax
# Example usage
parse_tree = syntax.parse_expression("((<>(p -> 0) -> 0) -> []p)")
print(parse_tree.proper_subformulas[1].val)
```
```plaintext
# Output
[]
```
### `tableau.isValid`
#### Description
Given a modal formuala $\varphi$ and Heyting algebra $\mathcal{H}$, checks if $\varphi$ is valid in the class of all $\mathcal{H}$-frames[^1].
Under the hood, it calls `tableau.construct_tableau` to construct a prefixed tableau for $\varphi$ and then returns `True` iff the constructed tableau is closed. `tableau.construct_tableau` is essentially the crux of this package.
#### Parameters
- `phi` (`str`, required): The modal formula $\varphi$, with syntax as described in the [`parameters`](#parameters-1) section of `syntax.parse_expression`.
- `H` (`algebra.HeytingAlgebra`, required) The Heyting algebra $\mathcal{H}$.
#### Returns
- (`boolean`) `True` if $\varphi$ is valid in the class of all $\mathcal{H}$-frames and `False` otherwise.
- (`tableau.Tableau`) The tableau constructed and used to determine validity.
#### Example
```python
from tableau import isValid
# Example usage
valid, tab = tableau.isValid("[]p -> p", H)
print(valid)
```
```plaintext
# Output
False
```
### `tableau.construct_counter_model`
#### Description
Given a modal formuala $\varphi$ and Heyting algebra $\mathcal{H}$, if possible produce an $\mathcal{H}-model$ in which $\varphi$ is is not globally true.
The model is read off of an open tableau for $\varphi$.
#### Parameters
- `phi` (`str`, required): The modal formula $\varphi$, with syntax as described in the [`parameters`](#parameters-1) section of `syntax.parse_expression`.
- `H` (`algebra.HeytingAlgebra`, required) The Heyting algebra $\mathcal{H}$.
- `tableau` (`tableau.Tableau`, optional) A tableau for $\varphi$. This is just used to prevent duplicate computations if the required tableau was already produced by `isValid`.
#### Returns
- (`algebra.HeytingAlgebra`) $\mathcal{H}$
- (`tuple[set[str], dict[TruthValue, dict[TruthValue, TruthValue]], dict[str, dict[str, TruthValue]]]`) The constructed counter $\mathcal{H}$-model.
#### Example
```python
from tableau import construct_counter_model
# Example usage
M = tableau.construct_counter_model("[]p -> p", H, tab)
print(M[1][1])
```
```plaintext
# Output
{'A': {'A': '0'}}
```
### `tableau.visualize_model`
#### Description
Produces a `matplotlib` visualizing a model returned by `tableau.construct_counter_model` as a labeled weighted directed graph.
#### Parameters
- `M` (`tuple[set[str], dict[TruthValue, dict[TruthValue, TruthValue]], dict[str, dict[str, TruthValue]]]`): An $\mathcal{H}$-model.
#### Returns
None
[^1]: See [[3]](#3) for appropriate definitions.
## For Developers
To run the code from source, follow these steps.
- Clone this repo.
```bash
git clone https://github.com/WeAreDevo/Many-Valued-Modal-Tableau.git
cd Many-Valued-Modal-Tableau
```
- Create a virtual enironment containing the required dependencies and activate it using either `conda`
```bash
conda env create -f environment.yml
conda activate mvmt
```
or using `virtualenv`
```bash
pip install virtualenv
virtualenv mvmt
source mvmt/bin/activate
pip install -r requirements.txt
```
- You can now edit the source code and run it locally. For example, run `main.py`:
```bash
python main.py "<expression>" --algebra filename.json --print_tableau --display_model
```
`<expression>` is the propositional modal formula you wish to check is valid.
`filename.json` should be the name of a file stored in `algebra_specs` that contains a json specification of a Heyting algebra.
The `--print_tableau` flag enables printing the constructed tableau to the terminal, and the `--display_model` flag enables displaying a counter model (if it exists) in a seperate window.
E.g.
```bash
python main.py "[]p->p" --algebra three_valued.json --print_tableau --display_model
```
### Note
`<expression>` should only contain well formed combinations of strings denoting:
- propositional variables, which must match the regex `[p-z]\d*` (i.e. begin with a letter between "p" and "z", followed by a string of zero or more decimal digits)
- a truth value from the specified algebra (see configurations below)
- a connective such as `"&"`, `"|"`, `"->"`, `"[]"`, `"<>"` (These corrrespond respectively to the syntactic objects $\land, \lor, \supset, \Box, \Diamond$ as presented in [[2]](#2))
- Matching parentheses `"("`,`")"`.
If some matching parentheses are not present, the usual order of precedence for propositional formulas is assumed.
## References
<a id="1">[1]</a>
Fitting, M. (1983). Prefixed Tableau Systems. In: Proof Methods for Modal and Intuitionistic Logics. Synthese Library, vol 169. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-2794-5_9
<a id="2">[2]</a>
Fitting, M. (1995). Tableaus for Many-Valued Modal Logic. Studia Logica: An International Journal for Symbolic Logic, 55(1), 63–87. http://www.jstor.org/stable/20015807
<a id="3">[3]</a>
Fitting, M. (1992). Many-valued modal logics II. Fundamenta Informaticae, 17, 55-73. https://doi.org/10.3233/FI-1992-171-205
## TODO
- Check if specified finite algebra is in fact a bounded distributive lattice (and hence Heyting algebra)
- Allow choice of stricter clsses of frames
Raw data
{
"_id": null,
"home_page": "",
"name": "mvmt",
"maintainer": "",
"docs_url": null,
"requires_python": ">=3.8",
"maintainer_email": "",
"keywords": "logic,modal logic,tableau",
"author": "",
"author_email": "Guy Axelrod <g.axelrod1@gmail.com>",
"download_url": "https://files.pythonhosted.org/packages/6f/e0/a05489c5f0c0cabea8226d6120a3a8880900cdc779ea3355d3c46c29ef72/mvmt-0.0.9.tar.gz",
"platform": null,
"description": "# Many-Valued Modal Tableau (mvmt)\n## Description\nThis repo contains the implementation of a desicion procedure for checking the validity of many-valued modal logic formulas. It is based on expansions of Fitting's work in [[1]](#1) and [[2]](#2). The proof of the correctness and termination of the procedure forms part of my master's dissertation which is in progress and will be linked after it has been submitted.\n\n## Installation\n```bash\npip install mvmt\n```\n\n## Getting Started\nIf you just want to use the package,\n`pip install mvmt` and use the modules provided. See the colab notebook for example usages.\n<a target=\"_blank\" href=\"https://colab.research.google.com/github/WeAreDevo/Many-Valued-Modal-Tableau/blob/main/mvmt_demo.ipynb\">\n <img src=\"https://colab.research.google.com/assets/colab-badge.svg\" alt=\"Open Demo In Colab\"/>\n</a>\n\nIf you would like to edit and run the source code directly, see the [For Developers](#for-developers) section.\n\n\n## Function Documentation\n\nThis section describes the useful functions provided by the package.\n### `utils.construct_heyting_algebra`\n\n#### Description\n\nA useful wrapper function for creating a `algebra.HeytingAlgebra` object from a user supplied `json` specification of a Heyting algebra. See below for the convention used to specify algebras in a `json` form.\n\n#### Parameters\n\n- `file_path` (`str`, optional): File path to `json` file containing a specification of a Heyting algebra.\n- `python_dict` (`dict`, optional): Python `dict` giving the `json` specification of a Heyting algebra. Default is `None`.\n\nAt least one of the arguments must be given. The specification should have the following format:\n```\n{\n \"elements\": [\"<t1>\",\"<t2>\",...,\"<tn>\"],\n \"order\": {\"<t1>\": [\"<t1_1>\",...,\"<t1_k1>\"], \"<t2>\": [\"<t2_1>\",...,\"<t2_k2>\"],...,\"<tn>\": [\"<tn_1>\",...,\"<tn_kn\">]},\n \"meet\": {\n \"<t1>\": {\"<t1>\": \"<m1_1>\", \"<t2>\": \"<m1_2>\", ..., \"<tn>\": \"<m1_n>\"},\n \"<t2>\": {\"<t1>\": \"<m2_1>\", \"<t2>\": \"<m2_2>\", ..., \"<tn>\": \"<m2_n>\"},\n .\n .\n .\n \"<tn>\": {\"<t1>\": \"<mn_1>\", \"<t2>\": \"<mn_2>\", ..., \"<tn>\": \"<mn_n>\"},\n },\n \"join\": {\n \"<t1>\": {\"<t1>\": \"<j1_1>\", \"<t2>\": \"<j1_2>\", ..., \"<tn>\": \"<j1_n>\"},\n \"<t2>\": {\"<t1>\": \"<j2_1>\", \"<t2>\": \"<j2_2>\", ..., \"<tn>\": \"<j2_n>\"},\n .\n .\n .\n \"<tn>\": {\"<t1>\": \"<jn_1>\", \"<t2>\": \"<jn_2>\", ..., \"<tn>\": \"<jn_n>\"},\n }\n}\n```\n\nWhere each angle bracket string in the above should be replaced with a string denoting a truth value. Such a string must match the regex `[a-o0-9]\\d*`. That is, it should be a string of decimal digits, or a letter between a and o (inclusive) followed by a string of decimal digits.\n\nIf we assume the json is intended to represent a heyting algebra $\\mathcal{H}=(H,\\land,\\lor,0,1, \\leq)$, and $I$ is the mapping from the strings denoting truth values to the actual truth values in $H$, then the json should be interpreted as follows:\n- $a \\in H$ iff $a=I$(\"<ti>\") for some `\"<ti>\"` in `elements`.\n- `\"<ti>\"` is in `order[\"<tk>\"]` iff $I$(\"<tk>\") $\\leq I$(\"<ti>\")\n- `meet[\"<ti>\"][\"<tk>\"]==\"<mi_k>\"` iff $I$(\"<mi_k>\") $= I$(\"<ti>\") $\\land I$(\"<tk>\")\n- `join[\"<ti>\"][\"<tk>\"]==\"<ji_k>\"` iff $I$(\"<ji_k>\") $= I$(\"<ti>\") $\\lor I$(\"<tk>\")\n\nFor example, a specification of the three-valued Heyting algebra $(\\{0,\\frac{1}{2},1\\}, \\land, \\lor, 0,1,\\leq)$ with $I(\\texttt{\"0\"})=0, I(\\texttt{\"a\"})=\\frac{1}{2}, I(\\texttt{\"1\"})=1$ is given by:\n```json\n{\n \"elements\": [\"0\",\"a\",\"1\"],\n \"order\": {\n \"0\": [\"0\",\"a\",\"1\"],\n \"a\": [\"a\",\"1\"],\n \"1\": [\"1\"]\n },\n \"meet\": {\n \"0\": {\"0\": \"0\",\"a\": \"0\",\"1\": \"0\"},\n \"a\": {\"0\": \"0\",\"a\": \"a\",\"1\": \"a\"},\n \"1\": {\"0\": \"0\",\"a\": \"a\",\"1\": \"1\"}\n },\n \"join\": {\n \"0\": {\"0\": \"0\",\"a\": \"a\",\"1\": \"1\"},\n \"a\": {\"0\": \"a\",\"a\": \"a\",\"1\": \"1\"},\n \"1\": {\"0\": \"1\",\"a\": \"1\",\"1\": \"1\"}\n }\n}\n```\n\n\n#### Note:\nOnly **one** of the `order`, `meet` or `join` fields needs to be specified and the other two can be left out of the `json`. If at least one of these is specified, the others can be uniquely determined. See the example code.\n\n#### Returns\n\n(`algebra.HeytingAlgebra`) A `algebra.HeytingAlgebra` object storing the algebra represented by the inputed specification.\n\n#### Example\n```python\nfrom mvmt import algebra, utils\n\n# Specification of a four-valued Heyting algebra\nspec = {\n \"elements\": [\"0\",\"a\",\"b\",\"1\"],\n \"order\": {\n \"0\": [\"0\",\"a\",\"b\",\"1\"], \n \"a\": [\"a\",\"1\"], \n \"b\": [\"b\",\"1\"], \n \"1\": [\"1\"]}\n}\n\n# Example usage\nH: algebra.HeytingAlgebra = utils.construct_heyting_algebra(python_dict=spec)\nprint(H.meet(algebra.TruthValue(\"a\"),algebra.TruthValue(\"b\")))\n```\n```plaintext\n# Output\n0\n```\n\n### `syntax.parse_expression`\n\n#### Description\n\nProduces the syntax parse tree of a modal formula.\n\n#### Parameters\n\n- `expression` (`str`, required): A modal formula.\n\n`expression` must belong to the language generated by the grammar\n```\nexpression ::= expression & expression\n | expression | expression\n | expression -> expression\n | [] expression\n | <> expression\n | (expression)\n | VAR\n | VALUE\n```\n`VAR` is a terminal symbol matching the regex `[p-z]\\d*`, denoting a propositional variable.\n\n`VALUE` is a terminal symbol matching the regex `[a-o0-9]\\d*`. It denotes a truth value from the algebra, and as such it must be the same as one of the strings given in `elements` of the algebra specification.\n\n#### Returns\n\n(`syntax.AST_Node`) The root node of the parse tree.\n\n#### Example\n```python\nfrom mvmt import syntax\n\n# Example usage\nparse_tree = syntax.parse_expression(\"((<>(p -> 0) -> 0) -> []p)\")\nprint(parse_tree.proper_subformulas[1].val)\n```\n```plaintext\n# Output\n[]\n```\n\n\n### `tableau.isValid`\n\n#### Description\n\nGiven a modal formuala $\\varphi$ and Heyting algebra $\\mathcal{H}$, checks if $\\varphi$ is valid in the class of all $\\mathcal{H}$-frames[^1].\n\nUnder the hood, it calls `tableau.construct_tableau` to construct a prefixed tableau for $\\varphi$ and then returns `True` iff the constructed tableau is closed. `tableau.construct_tableau` is essentially the crux of this package.\n\n#### Parameters\n\n- `phi` (`str`, required): The modal formula $\\varphi$, with syntax as described in the [`parameters`](#parameters-1) section of `syntax.parse_expression`.\n- `H` (`algebra.HeytingAlgebra`, required) The Heyting algebra $\\mathcal{H}$.\n\n#### Returns\n\n- (`boolean`) `True` if $\\varphi$ is valid in the class of all $\\mathcal{H}$-frames and `False` otherwise.\n- (`tableau.Tableau`) The tableau constructed and used to determine validity.\n\n#### Example\n```python\nfrom tableau import isValid\n\n# Example usage\nvalid, tab = tableau.isValid(\"[]p -> p\", H)\nprint(valid)\n```\n```plaintext\n# Output\nFalse\n```\n\n\n### `tableau.construct_counter_model`\n\n#### Description\n\nGiven a modal formuala $\\varphi$ and Heyting algebra $\\mathcal{H}$, if possible produce an $\\mathcal{H}-model$ in which $\\varphi$ is is not globally true.\nThe model is read off of an open tableau for $\\varphi$.\n\n#### Parameters\n\n- `phi` (`str`, required): The modal formula $\\varphi$, with syntax as described in the [`parameters`](#parameters-1) section of `syntax.parse_expression`.\n- `H` (`algebra.HeytingAlgebra`, required) The Heyting algebra $\\mathcal{H}$.\n- `tableau` (`tableau.Tableau`, optional) A tableau for $\\varphi$. This is just used to prevent duplicate computations if the required tableau was already produced by `isValid`.\n\n#### Returns\n\n- (`algebra.HeytingAlgebra`) $\\mathcal{H}$\n- (`tuple[set[str], dict[TruthValue, dict[TruthValue, TruthValue]], dict[str, dict[str, TruthValue]]]`) The constructed counter $\\mathcal{H}$-model.\n\n#### Example\n```python\nfrom tableau import construct_counter_model\n\n# Example usage\nM = tableau.construct_counter_model(\"[]p -> p\", H, tab)\nprint(M[1][1])\n```\n```plaintext\n# Output\n{'A': {'A': '0'}}\n```\n\n### `tableau.visualize_model`\n\n#### Description\n\nProduces a `matplotlib` visualizing a model returned by `tableau.construct_counter_model` as a labeled weighted directed graph.\n\n#### Parameters\n\n- `M` (`tuple[set[str], dict[TruthValue, dict[TruthValue, TruthValue]], dict[str, dict[str, TruthValue]]]`): An $\\mathcal{H}$-model.\n\n#### Returns\nNone\n\n[^1]: See [[3]](#3) for appropriate definitions.\n## For Developers\nTo run the code from source, follow these steps.\n- Clone this repo.\n```bash\ngit clone https://github.com/WeAreDevo/Many-Valued-Modal-Tableau.git\ncd Many-Valued-Modal-Tableau\n```\n- Create a virtual enironment containing the required dependencies and activate it using either `conda` \n```bash\nconda env create -f environment.yml\nconda activate mvmt\n```\nor using `virtualenv`\n```bash\npip install virtualenv\nvirtualenv mvmt\nsource mvmt/bin/activate\npip install -r requirements.txt\n```\n\n- You can now edit the source code and run it locally. For example, run `main.py`:\n```bash\npython main.py \"<expression>\" --algebra filename.json --print_tableau --display_model\n``` \n`<expression>` is the propositional modal formula you wish to check is valid.\n`filename.json` should be the name of a file stored in `algebra_specs` that contains a json specification of a Heyting algebra.\nThe `--print_tableau` flag enables printing the constructed tableau to the terminal, and the `--display_model` flag enables displaying a counter model (if it exists) in a seperate window.\n\nE.g.\n```bash\npython main.py \"[]p->p\" --algebra three_valued.json --print_tableau --display_model\n```\n\n\n### Note\n`<expression>` should only contain well formed combinations of strings denoting:\n - propositional variables, which must match the regex `[p-z]\\d*` (i.e. begin with a letter between \"p\" and \"z\", followed by a string of zero or more decimal digits)\n - a truth value from the specified algebra (see configurations below)\n - a connective such as `\"&\"`, `\"|\"`, `\"->\"`, `\"[]\"`, `\"<>\"` (These corrrespond respectively to the syntactic objects $\\land, \\lor, \\supset, \\Box, \\Diamond$ as presented in [[2]](#2))\n - Matching parentheses `\"(\"`,`\")\"`.\n\nIf some matching parentheses are not present, the usual order of precedence for propositional formulas is assumed.\n\n## References\n<a id=\"1\">[1]</a> \nFitting, M. (1983). Prefixed Tableau Systems. In: Proof Methods for Modal and Intuitionistic Logics. Synthese Library, vol 169. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-2794-5_9\n\n<a id=\"2\">[2]</a> \nFitting, M. (1995). Tableaus for Many-Valued Modal Logic. Studia Logica: An International Journal for Symbolic Logic, 55(1), 63\u201387. http://www.jstor.org/stable/20015807\n\n<a id=\"3\">[3]</a> \nFitting, M. (1992). Many-valued modal logics II. Fundamenta Informaticae, 17, 55-73. https://doi.org/10.3233/FI-1992-171-205\n\n\n## TODO\n- Check if specified finite algebra is in fact a bounded distributive lattice (and hence Heyting algebra)\n- Allow choice of stricter clsses of frames",
"bugtrack_url": null,
"license": "",
"summary": "A package for checking the validity of many-valued modal formulas",
"version": "0.0.9",
"project_urls": {
"Bug Tracker": "https://github.com/WeAreDevo/Many-Valued-Modal-Tableau/issues",
"Homepage": "https://github.com/WeAreDevo/Many-Valued-Modal-Tableau",
"repository": "https://github.com/WeAreDevo/Many-Valued-Modal-Tableau"
},
"split_keywords": [
"logic",
"modal logic",
"tableau"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "31e0b59f241e27711000c1ce708225f23fd8bed7e38b1d88185a8e0648fa69c4",
"md5": "e2485905f8742a0071831602eef69651",
"sha256": "ef47ce33c32136670e44f65cb7b0aca57e5b8bbc0b5b21c23f091d4cd346c800"
},
"downloads": -1,
"filename": "mvmt-0.0.9-py3-none-any.whl",
"has_sig": false,
"md5_digest": "e2485905f8742a0071831602eef69651",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.8",
"size": 16813,
"upload_time": "2023-10-06T10:19:58",
"upload_time_iso_8601": "2023-10-06T10:19:58.018497Z",
"url": "https://files.pythonhosted.org/packages/31/e0/b59f241e27711000c1ce708225f23fd8bed7e38b1d88185a8e0648fa69c4/mvmt-0.0.9-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "6fe0a05489c5f0c0cabea8226d6120a3a8880900cdc779ea3355d3c46c29ef72",
"md5": "383a5aab5aa88849ed7af8124902cdcc",
"sha256": "36880048692a7af4ec676e3023de7f6461b0c72ef66ec7125a0150072da8db5a"
},
"downloads": -1,
"filename": "mvmt-0.0.9.tar.gz",
"has_sig": false,
"md5_digest": "383a5aab5aa88849ed7af8124902cdcc",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.8",
"size": 18336,
"upload_time": "2023-10-06T10:20:00",
"upload_time_iso_8601": "2023-10-06T10:20:00.097881Z",
"url": "https://files.pythonhosted.org/packages/6f/e0/a05489c5f0c0cabea8226d6120a3a8880900cdc779ea3355d3c46c29ef72/mvmt-0.0.9.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2023-10-06 10:20:00",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "WeAreDevo",
"github_project": "Many-Valued-Modal-Tableau",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"requirements": [],
"lcname": "mvmt"
}
