Conditional Narrowing in Rewriting Logic and Maude
Author: Luis Manuel Aguirre
Advisors: Narciso Martí-Oliet, Miguel Palomino, Isabel Pita
This is a companion site to the following work:
2021:
- AVERTIS 2019 paper “Strategies in Conditional Narrowing Modulo SMT Plus Axioms”
2017:
- PPDP 2017 paper “Conditional Narrowing Modulo SMT and Axioms”
2014:
- WRLA 2014 paper “Conditional Narrowing Modulo in Rewriting Logic and Maude”
2013:
- The master thesis “Conditional Narrowing in Rewriting Logic and Maude”
Links for the AVERTIS 2019 paper::
Instructions to run the examples of the AVERTIS 2019 paper and the Technical Report::
- The Maude system 3.1 must be installed. It is available for download here.
- Give execution permisions to the maude binary, e.g., 'chmod 755 maude.linux64'.
- Unzip the 'prototype_AVERTIS.zip' file and copy its contents to the Maude system folder.
- Follow the instructions in the newly created 'example.txt' file in the Maude system folder.
Links for the PPDP 2017 prototypes (narrowing with SMT solvers)::
Instructions to run the examples of the PPDP 2017 prototypes::
- Unzip the 'prototypes_PPDP17.zip' file and go to the folder with all the files.
- Give execution permisions to the maude binary, e.g., 'chmod 755 maude-Yices2.linux64'.
- There are two example files: 'exampleToasts-red.maude' and 'exampleToasts-rew.maude'.
- Each example file can be edited to select the desired protopype version on line 5.
- Each example file has several problems. You can uncomment any of them to check the prototype.
- Once finished editing the example file launch maude with it, e.g., './maude-Yices2.linux64 exampleToasts-rew.maude'.
Links for the WRLA 2014 paper::
Links for the 2013 master thesis::
Instructions to run the examples of the 2013 master thesis::
- The Maude system 2.6 must be installed. It is available for download here.
- Unzip axr.zip on the same folder where the Maude system is installed.
- Run Maude.
- Unzip and open any of the example .txt files.
- In Maude's command line, follow the instructions for any of the example modules.