TY - JOUR
T1 - Generalized rewrite theories, coherence completion, and symbolic methods
AU - Meseguer, José
N1 - Funding Information:
I thank the referees for their constructive criticism and valuable suggestions to improve the paper. This work has been partially supported by NRL under contract number N00173-17-1-G002 .
Publisher Copyright:
© 2019
PY - 2020/1
Y1 - 2020/1
N2 - A new notion of generalized rewrite theory suitable for symbolic reasoning and generalizing the standard notion in [19] is motivated and defined. Also, new requirements for symbolic executability of generalized rewrite theories that extend those in [33] for standard rewrite theories, including a generalized notion of coherence, are given. Symbolic executability, including coherence, is both ensured and made available for a wide class of such theories by automatable theory transformations. Using these foundations, several symbolic reasoning methods using generalized rewrite theories are studied, including: (i) symbolic description of sets of terms by pattern predicates; (ii) reasoning about universal reachability properties by generalized rewriting; (iii) reasoning about existential reachability properties by constrained narrowing; and (iv) symbolic verification of safety properties such as invariants and stability properties.
AB - A new notion of generalized rewrite theory suitable for symbolic reasoning and generalizing the standard notion in [19] is motivated and defined. Also, new requirements for symbolic executability of generalized rewrite theories that extend those in [33] for standard rewrite theories, including a generalized notion of coherence, are given. Symbolic executability, including coherence, is both ensured and made available for a wide class of such theories by automatable theory transformations. Using these foundations, several symbolic reasoning methods using generalized rewrite theories are studied, including: (i) symbolic description of sets of terms by pattern predicates; (ii) reasoning about universal reachability properties by generalized rewriting; (iii) reasoning about existential reachability properties by constrained narrowing; and (iv) symbolic verification of safety properties such as invariants and stability properties.
KW - Coherence
KW - Constrained narrowing
KW - Generalized rewrite theories
KW - Pattern predicates
KW - Symbolic invariant verification
UR - http://www.scopus.com/inward/record.url?scp=85081571697&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85081571697&partnerID=8YFLogxK
U2 - 10.1016/j.jlamp.2019.100483
DO - 10.1016/j.jlamp.2019.100483
M3 - Article
AN - SCOPUS:85081571697
SN - 2352-2208
VL - 110
JO - Journal of Logical and Algebraic Methods in Programming
JF - Journal of Logical and Algebraic Methods in Programming
M1 - 100483
ER -