Difference between revisions of "Term Rewriting"
From Termination-Portal.org
Jump to navigationJump to search (Created page with '(no content yet) Category:Categories') |
|||
| Line 1: | Line 1: | ||
| − | + | We use an adaption of the [https://project-coco.uibk.ac.at/ARI/ ARI format]. Our format differs from the formt used at COCO as follows: | |
| − | [ | + | * We do not impose any variable conditions, so a rewrite rule is a pair of arbitrary terms. |
| + | * Identifiers (i.e., names of variables or function symbols) must be valid [https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf SMT-LIB symbols], whereas COCO uses a more liberal definition. Both simple and quoted symbols are allowed. | ||
| + | * Rules are annotated with optional costs, which are natural numbers. So rules are defined as follows: | ||
| + | <code> | ||
| + | rule ::= ( rule term term cost?) | ||
| + | cond ::= :cost number | ||
| + | </code> | ||
Revision as of 19:03, 15 April 2024
We use an adaption of the ARI format. Our format differs from the formt used at COCO as follows:
- We do not impose any variable conditions, so a rewrite rule is a pair of arbitrary terms.
- Identifiers (i.e., names of variables or function symbols) must be valid SMT-LIB symbols, whereas COCO uses a more liberal definition. Both simple and quoted symbols are allowed.
- Rules are annotated with optional costs, which are natural numbers. So rules are defined as follows:
rule ::= ( rule term term cost?)
cond ::= :cost number
