TY - GEN
T1 - Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
AU - Meseguer, José
AU - Skeirik, Stephen
N1 - Acknowledgements. We cordially thank the referees for their very helpful suggestions to improve the paper. Work partially supported by NRL under contract N00173-17-1-G002.
PY - 2020
Y1 - 2020
N2 - We present an inductive inference system for proving validity of formulas in the initial algebra TE of an order-sorted equational theory E with 17 inference rules, where only 6 of them require user interaction, while the remaining 11 can be automated as simplification rules and can be combined together as a limited, yet practical, automated inductive theorem prover. The 11 simplification rules are based on powerful equational reasoning techniques, including: equationally defined equality predicates, constructor variant unification, variant satisfiability, order-sorted congruence closure, contextual rewriting and recursive path orderings. For E= (Σ, E⊎ B), these techniques work modulo B, with B a combination of associativity and/or commutativity and/or identity axioms.
AB - We present an inductive inference system for proving validity of formulas in the initial algebra TE of an order-sorted equational theory E with 17 inference rules, where only 6 of them require user interaction, while the remaining 11 can be automated as simplification rules and can be combined together as a limited, yet practical, automated inductive theorem prover. The 11 simplification rules are based on powerful equational reasoning techniques, including: equationally defined equality predicates, constructor variant unification, variant satisfiability, order-sorted congruence closure, contextual rewriting and recursive path orderings. For E= (Σ, E⊎ B), these techniques work modulo B, with B a combination of associativity and/or commutativity and/or identity axioms.
UR - https://www.scopus.com/pages/publications/85099053772
UR - https://www.scopus.com/pages/publications/85099053772#tab=citedBy
U2 - 10.1007/978-3-030-63595-4_7
DO - 10.1007/978-3-030-63595-4_7
M3 - Conference contribution
AN - SCOPUS:85099053772
SN - 9783030635947
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 114
EP - 135
BT - Rewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers
A2 - Escobar, Santiago
A2 - Martí-Oliet, Narciso
PB - Springer
T2 - 13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020
Y2 - 20 October 2020 through 22 October 2020
ER -