brozek/vspursuer
1
0
Fork 0
mirror of https://github.com/Brandon-Rozek/matmod.git synced 2026-01-28 07:32:56 +00:00
Code Issues Projects Releases Packages Wiki Activity
Matrix Model Generator for Implicative Connectives
119 commits 8 branches 2 tags 306 KiB
Find a file
Exact
Brandon Rozek 42f063408b
(#46) Finding models via Z3 
Uses Z3 to find a model of a certain size for a given logic. This PR also introduces falsification rules and the ability to directly check via SMT whether a logic has VSP instead of generating models first.
2026-01-27 15:28:46 -05:00
examples Added another example 2024-10-15 10:30:14 -04:00
utils Skip model sizes 2-5 and 7 when conjunction, disjunction, and negation are defined 2025-12-12 11:36:21 -05:00
.gitignore Initial commit 2024-04-08 23:59:21 -04:00
common.py Check models in parallel 2024-11-26 16:24:49 -05:00
generate_model.py Updated driver file R.py to showcase SMT techinques 2026-01-27 12:48:33 -05:00
logic.py Updated driver file R.py to showcase SMT techinques 2026-01-27 12:48:33 -05:00
model.py Refactored out valuation generation code in SMT 2026-01-27 15:22:47 -05:00
parse_magic.py Check VSP for non-MaGICal models via SMT 2026-01-12 16:55:37 -05:00
R.py Updated driver file R.py to showcase SMT techinques 2026-01-27 12:48:33 -05:00
README.md Updated interface 2024-11-05 13:19:44 -05:00
smt.py Refactored out valuation generation code in SMT 2026-01-27 15:22:47 -05:00
vsp.py Small comment change 2026-01-27 15:26:16 -05:00
vspursuer.py Skip model sizes 2-5 and 7 when conjunction, disjunction, and negation are defined 2025-12-12 11:36:21 -05:00

README.md

VSPursuer: Verify Relevance Properties for Matrix Models with Implicative Connectives

Interested in seeing which satisfiable models from arranstewart/magic have the variable sharing property?

(1) Generate satisfiable matrix models using MaGIC.

  • Use the ugly data format as the output

(2) Run our tool! It will first attempt to parse all the matrices in the output file and then check for the variable sharing property one-by-one.

./vspursuer.py -i examples/R6

If you face any troubles, feel free to reach out. This tool also is able to generate satisfiable models given a specification (see: R.py). This is, however, much slower than MaGIC so you're better off using that.

Check out the GitHub issue tracker to see upcoming features or make your own requests.