On a Generalised Logicality Theorem

  • Marc Aiguier
  • Diane Bahrami
  • Catherine Dubois
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2385)


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.


Formal system semi-commutation abstract rewrite tree abstract convertibility relation logicality 


Term Rewriting Reasoning Integration of Logical Reasoning and Computer Algebra 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Aiguier, D. Bahrami and C. Dubois, On the General Structure of Rewrite Proofs. Technical report, University of Evry, 2001.
  2. 2.
    E. Astesiano and M. Cerioli, Free Objects and Equational Deduction for Partial Conditional Specifications. TCS, 152(1):91–138. Amsterdam: Elsevier, 1995.Google Scholar
  3. 3.
    F. Baader and T. Nipkow, Term Rewriting and All That. Cambridge University Press, 1998.Google Scholar
  4. 4.
    L. Bachmair and H. Ganzinger, Rewrite techniques for transitive relations. 9th IEEE Symposium on Logic in Computer Science, pp. 384–393, 1994.Google Scholar
  5. 5.
    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
  6. 6.
    S. Kaplan, Simplifying Conditional Term Rewriting Systems: Unification, Simplification and Confluence. Journal of Symbolic Computation, 4(3):295–334. Amsterdam: Academic Press, 1987.Google Scholar
  7. 7.
    J. Levy and J. Agusti, Bi-rewriting systems. Journal of Symbolic Computation, 22(3):279–314. Amsterdam: Academic Press, 1996.Google Scholar
  8. 8.
    J. Meseguer, Conditional rewriting logic as a unified model of concurrency. TCS, 96(1):73–155. Amsterdam: Elsevier, 1992.Google Scholar
  9. 9.
    V. van Oostrom, Sub-Birkhoff. Draft, 13 pages, 18 December 2000, available at
  10. 10.
    M. Schorlemmer, On Specifying and Reasoning with Special Relations. PhD thesis, Institut d’Investigaciò en Intel.ligència Artificial, University of Catalunya, 1999.Google Scholar
  11. 11.
    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.Google Scholar
  12. 12.
    G. Struth, Canonical Transformations in Algebra, Universal Algebra and Logic. PhD thesis, Institut für Informatik, University of Saarland, 1998.Google Scholar
  13. 13.
    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.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Marc Aiguier
    • 1
  • Diane Bahrami
    • 1
  • Catherine Dubois
    • 2
  1. 1.CNRS UMR 8042, LaMIUniversité d’Évry Val d’EssonneÉvryFrance
  2. 2.Institut d’Informatique d’EntrepriseCEDRICÉvryFrance

Personalised recommendations