New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

tracking: rewriting #61

Open

5 tasks

c-cube opened this issue Aug 1, 2019 · 0 comments

Labels

I-rewriting research

Member

c-cube commented Aug 1, 2019

conditional rewriting
- parse rewrite forall vars. ∧_i a_i => l = r
- same for clausal rewriting
- handling by inference rule that unifies (rewrite & narrowing are the same)
```
`∧_i a_i => l = r           C[l]    lσ=a
----------------------------------------
    ∧_i a_iσ => C[rσ]
```
  which is a form of superposition that is artificially restricted to
  rewriting l first
- for each rule, compile fast pre-checks (e.g.
  matched term must have symbol f at arg position i) and use
  these before attempting call to matching
- in proof, put set of rewrite rules used in simplification steps,
  at least in full (non-compressed) version

The text was updated successfully, but these errors were encountered:

c-cube added research I-rewriting labels

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment