Abstract
In this paper, the correspondence between derivability (syntactic consequences obtained from ⊢) and convertibility in rewriting \( \left( {\mathop \leftrightarrow \limits^* } \right) \) , the so-called logicality, is studied in a generic way (i.e. logic-independent). This is achieved by giving simple conditions to characterise logics where (bidirectional) rewriting can be applied. These conditions are based on a property defined on proof trees, that we call semi-commutation. Then, we show that the convertibility relation obtained via semi-commutation is equivalent to the inference relation ⊢ of the logic under consideration.
This work was partially supported by the European Commission under WGs Aspire (22704) and is partially supported by the French research program “GDR Algorithmique-Langage-Programmation (ALP)”
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Aiguier, D. Bahrami and C. Dubois, On the General Structure of Rewrite Proofs. Technical report, University of Evry, 2001. ftp://ftp.lami.univ-evry.fr/pub/publi-cations/reports/2001/index.html/lami_58.ps.gz.
E. Astesiano and M. Cerioli, Free Objects and Equational Deduction for Partial Conditional Specifications. TCS, 152(1):91–138. Amsterdam: Elsevier, 1995.
F. Baader and T. Nipkow, Term Rewriting and All That. Cambridge University Press, 1998.
L. Bachmair and H. Ganzinger, Rewrite techniques for transitive relations. 9th IEEE Symposium on Logic in Computer Science, pp. 384–393, 1994.
F. Barbier, Méta-réécriture: application á la logique des relations spéciales. Master thesis, University of Evry, 2001. Supervised by M. Aiguier and D. Bahrami (In french), avalaible at http://www.lami.univ-evry.fr/~fbarbier/recherche-fr.html
S. Kaplan, Simplifying Conditional Term Rewriting Systems: Unification, Simplification and Confluence. Journal of Symbolic Computation, 4(3):295–334. Amsterdam: Academic Press, 1987.
J. Levy and J. Agusti, Bi-rewriting systems. Journal of Symbolic Computation, 22(3):279–314. Amsterdam: Academic Press, 1996.
J. Meseguer, Conditional rewriting logic as a unified model of concurrency. TCS, 96(1):73–155. Amsterdam: Elsevier, 1992.
V. van Oostrom, Sub-Birkhoff. Draft, 13 pages, 18 December 2000, available at http://www.phil.uu.nl/~oostrom/publication/rewriting.html.
M. Schorlemmer, On Specifying and Reasoning with Special Relations. PhD thesis, Institut d’Investigaciò en Intel.ligència Artificial, University of Catalunya, 1999.
G. Struth, Knuth-Bendix Completion for Non-Symmetric Transitive Relations. Proceedings of the Second International Workshop on Rule-Based Programming (RULE2001), Electronic Notes in TCS, 59(4). Elsevier 2001.
G. Struth, Canonical Transformations in Algebra, Universal Algebra and Logic. PhD thesis, Institut für Informatik, University of Saarland, 1998.
T. Yamada, J. Avenhaus, C. Loría-Sáenz, and A. Middeldorp, Logicality of Conditional Rewrite Systems. TCS, 236(1,2):209–232. Amsterdam: Elsevier, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aiguier, M., Bahrami, D., Dubois, C. (2002). On a Generalised Logicality Theorem. In: Calmet, J., Benhamou, B., Caprotti, O., Henocque, L., Sorge, V. (eds) Artificial Intelligence, Automated Reasoning, and Symbolic Computation. AISC Calculemus 2002 2002. Lecture Notes in Computer Science(), vol 2385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45470-5_8
Download citation
DOI: https://doi.org/10.1007/3-540-45470-5_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43865-6
Online ISBN: 978-3-540-45470-0
eBook Packages: Springer Book Archive