Conditional Narrowing in Rewriting Logic and Maude

This is a companion site to the following work:

2021:

- AVERTIS 2019 paper “Strategies in Conditional Narrowing Modulo SMT Plus Axioms”

- 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::

• Technical Report with full proofs as a PDF file.
• Prototype with examples and instructions as a ZIP file.

Instructions to run the examples of the AVERTIS 2019 paper and the Technical Report::

1. The Maude system 3.1 must be installed. It is available for download here.
2. Give execution permisions to the maude binary, e.g., 'chmod 755 maude.linux64'.
3. Unzip the 'prototype_AVERTIS.zip' file and copy its contents to the Maude system folder.
4. 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)::

• Prototypes with examples and instructions as a ZIP file.

Instructions to run the examples of the PPDP 2017 prototypes::

1. Unzip the 'prototypes_PPDP17.zip' file and go to the folder with all the files.
2. Give execution permisions to the maude binary, e.g., 'chmod 755 maude-Yices2.linux64'.
3. There are two example files: 'exampleToasts-red.maude' and 'exampleToasts-rew.maude'.
4. Each example file can be edited to select the desired protopype version on line 5.
5. Each example file has several problems. You can uncomment any of them to check the prototype.
6. Once finished editing the example file launch maude with it, e.g., './maude-Yices2.linux64 exampleToasts-rew.maude'.

Links for the WRLA 2014 paper::

• Preproceedings version as a PDF file.
• Preproceedings version with full proofs as a PDF file.
• Presentation slides as a PDF file.

Links for the 2013 master thesis::

• The master thesis as a PDF file.
• The prototype: all Maude modules needed for the prototype to run (zipped).
• Examples: examples from the master thesis (zipped).

Instructions to run the examples of the 2013 master thesis::

1. The Maude system 2.6 must be installed. It is available for download here.
2. Unzip axr.zip on the same folder where the Maude system is installed.
3. Run Maude.
4. Unzip and open any of the example .txt files.
5. In Maude's command line, follow the instructions for any of the example modules.