Academic Journal
Equational Theories and Validity for Logically Constrained Term Rewriting
| العنوان: | Equational Theories and Validity for Logically Constrained Term Rewriting |
|---|---|
| المؤلفون: | Aoto, Takahito, Nishida, Naoki, Schöpf, Jonas |
| المساهمون: | Takahito Aoto and Naoki Nishida and Jonas Schöpf |
| بيانات النشر: | Schloss Dagstuhl – Leibniz-Zentrum für Informatik |
| سنة النشر: | 2024 |
| المجموعة: | DROPS - Dagstuhl Research Online Publication Server (Schloss Dagstuhl - Leibniz Center for Informatics ) |
| مصطلحات موضوعية: | constrained equation, constrained equational theory, logically constrained term rewriting, algebraic semantics, consistency |
| الوصف: | Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity analysis and confluence analysis for logically constrained term rewriting, these works solely focus on the syntactic side of the formalism lacking detailed investigations on semantics. In this paper, we investigate a semantic side of logically constrained term rewriting. To this end, we first define constrained equations, constrained equational theories and validity of the former based on the latter. After presenting the relationship of validity and conversion of rewriting, we then construct a sound inference system to prove validity of constrained equations in constrained equational theories. Finally, we give an algebraic semantics, which enables one to establish invalidity of constrained equations in constrained equational theories. This algebraic semantics derives a new notion of consistency for constrained equational theories. |
| نوع الوثيقة: | article in journal/newspaper conference object |
| وصف الملف: | application/pdf |
| اللغة: | English |
| Relation: | Is Part Of LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024); https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.31 |
| DOI: | 10.4230/LIPIcs.FSCD.2024.31 |
| الاتاحة: | https://doi.org/10.4230/LIPIcs.FSCD.2024.31 https://nbn-resolving.org/urn:nbn:de:0030-drops-203607 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.31 |
| Rights: | https://creativecommons.org/licenses/by/4.0/legalcode |
| رقم الانضمام: | edsbas.4DBEAFA3 |
| قاعدة البيانات: | BASE |
| DOI: | 10.4230/LIPIcs.FSCD.2024.31 |
|---|