Welcome, ISR 2019 participants!

Lecture slides.

(Selected) bibliography on LCTRSs.

Lecture based on:

• Stefan Ciobaca and Dorel Lucanu. A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems. IJCAR 2018;
• Stefan Ciobaca, Andrei Arusoaie, and Dorel Lucanu. Unification Modulo Builtins. WoLLIC 2018.

Some other recent related work:

• Luis Aguirre, Narciso Mart-Oliet, Miguel Palomino, and Isabel Pita. Conditional Narrowing Modulo SMT and Axioms. PPDP 2017;
• Kyungmin Bae and Camilo Rocha. Guarded Terms for Rewriting Modulo SMT. FACS 2017;
• Claude Kirchner, Helene Kirchner, and Michael Rusinowitch. Deduction with Symbolic Constraints. Technical Report RR-1358, INRIA, 1990;
• Cynthia Kop. Termination of LCTRSs. CoRR, abs/1601.03206, 2016;
• Cynthia Kop and Naoki Nishida. Term Rewriting with Logical Constraints.FroCoS 2013;
• Cynthia Kop and Naoki Nishida. Constrained Term Rewriting tooL. LPAR2015;
• Jose Meseguer. Generalized rewrite theories and coherence completion. In: Rewrit- ing Logic and Its Applications - 12th International Workshop, WRLA 2018.
• Camilo Rocha, Jose Meseguer, and Cesar A. Munoz. Rewriting modulo SMT and open system analysis. J. Log. Algebr. Meth. Program., 86(1):269–297, 2017;
• Stephen Skeirik, Andrei Stefanescu, and Jose Meseguer. A constructor-based reach-ability logic for rewrite theories. TR. http://hdl.handle.net/2142/95770;

Download, compile, install and test RMT.

Prerequisites

• A modern C++ compiler (a recent version of g++, clang or MSVC will do);
• git;
• CMake
• Z3

Installation and Compilation

We list the exact steps for an Ubuntu machine. Please adapt for use on Mac or Windows.

• Step 1: Install build-essential (g++) and cmake
sudo apt install build-essential cmake
• Step 2: Clone the Z3 repository in ~/z3
git clone https://github.com/Z3Prover/z3.git
• Step 3: Compile Z3 in ~/z3/build (4 parallel compilation processes)
cd z3 mkdir build cd build cmake .. make -j 4 cd ../..
This step might take around 10 minutes, depending on your exact machine.
• Step 4: Clone the RMT repository in ~/rmt
git clone https://github.com/ciobaca/rmt.git
• Step 5: Build RMT (links against Z3, previously compiled)
cd rmt mkdir build cd build cmake .. -DZ3_DIR=~/z3/build make -j 4 cd ../..
• Step 6: running RMT
cd rmt/examples/ ~/rmt/build/fastrmt -v 0 isr2019/exercise1.rmt
This will will rmt with verbosity 0 (lowest) on the given example.