Combining Decision Procedures for Positive Theories Sharing Constructors

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Toggle side column

Combining Decision Procedures for Positive Theories Sharing Constructors

Franz BaaderFranz Baader,  Cesare TinelliCesare Tinelli
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
  • 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: Automatentheorie
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},
}