A package for checking the validity of many-valued modal formulas
Project description
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] and [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
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.
If you would like to edit and run the source code directly, see the 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 tojson
file containing a specification of a Heyting algebra.python_dict
(dict
, optional): Pythondict
giving thejson
specification of a Heyting algebra. Default isNone
.
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>"
inelements
. "<ti>"
is inorder["<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:
{
"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
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")))
# 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
from mvmt import syntax
# Example usage
parse_tree = syntax.parse_expression("((<>(p -> 0) -> 0) -> []p)")
print(parse_tree.proper_subformulas[1].val)
# 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 theparameters
section ofsyntax.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 andFalse
otherwise. - (
tableau.Tableau
) The tableau constructed and used to determine validity.
Example
from tableau import isValid
# Example usage
valid, tab = tableau.isValid("[]p -> p", H)
print(valid)
# 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 theparameters
section ofsyntax.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 byisValid
.
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
from tableau import construct_counter_model
# Example usage
M = tableau.construct_counter_model("[]p -> p", H, tab)
print(M[1][1])
# 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] for appropriate definitions.
For Developers
To run the code from source, follow these steps.
- Clone this repo.
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
conda env create -f environment.yml
conda activate mvmt
or using virtualenv
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
:
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.
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]) - Matching parentheses
"("
,")"
.
If some matching parentheses are not present, the usual order of precedence for propositional formulas is assumed.
References
[1] 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
[2] 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
[3] 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
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.