Combining Decision Procedures for Positive Theories Sharing Constructors

Franz BaaderFranz Baader, Cesare TinelliCesare Tinelli

Datei:BaaderTinelliRTA02.ps.gz

Download

Franz Baader, Cesare Tinelli
Combining Decision Procedures for Positive Theories Sharing Constructors
In S. Tison, eds., Proceedings of the 13th International Conference on Rewriting Techniques and Applications (RTA-02), volume 2378 of Lecture Notes in Computer Science, 338-352, 2002. Springer

Details
Bibtex

KurzfassungAbstract
This paper addresses the following combination problem: given two equational theories E1 and E2 whose positive theories are decidable, how can one obtain a decision procedure for the positive theory of their union. For theories over disjoint signatures, this problem was solved by Baader and Schulz in 1995. This paper is a first step towards extending this result to the case of theories sharing constructors. Since there is a close connection between positive theories and unification problems, this also extends to the non-disjoint case the work on combining decision procedures for unification modulo equational theories.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ BaaderTinelliRTA02,
  address = {Copenhagen, Denmark},
  author = {F. {Baader} and C. {Tinelli}},
  booktitle = {Proceedings of the 13th International Conference on Rewriting Techniques and Applications (RTA-02)},
  editor = {S. {Tison}},
  pages = {338--352},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {Combining Decision Procedures for Positive Theories Sharing Constructors},
  volume = {2378},
  year = {2002},
}