From d14ad5279834c8d83e4f79f8b447db76b97ad376 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sat, 15 Jun 2024 09:02:31 -0700 Subject: [PATCH] Updated README --- README.md | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 0c12b56..3dd895f 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,16 @@ -# Matmod: Matrix Model Generator for Implicative Connectives +# Matmod: Verify Relevance Properties for Matrix Models with Implicative Connectives -This repository is mostly an experiment to help -me better understand matrix models. +Interested in seeing which satisfiable models from [arranstewart/magic](https://github.com/arranstewart/magic) have the variable sharing property? -You're likely better off using [arranstewart/magic](https://github.com/arranstewart/magic). +(1) Generate satisfiable matrix models using `magic`. + - Use the `ugly` data format as the output + - Keep in mind not all logic features in magic are supported, check out the [GitHub issue tracker](https://github.com/Brandon-Rozek/matmod/issues) to see upcoming features or make your own requests -We support output from magic using the ugly data format. +(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. ``` python3 parse_magic.py < UGLY_FILE_FROM_MAGIC ``` + +If you face any troubles, feel free to reach out. This tool also has capabilities to generate satisfiable models given a specification (see: R.py), however, it is much slower than magic so you're better off using that. +