Skip to main content
SpringerLink
Log in

Unification in a combination of equational theories with shared constants and its application to primal algebras

  • Session 10: Unification and Equality I
  • Conference paper
  • First Online:
Logic Programming and Automated Reasoning (LPAR 1992)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 624))

Abstract

We extend the results on combination of disjoint equational theories to combination of equational theories where the only function symbols shared are constants. This is possible because there exist finitely many proper shared terms (the constants) which can be assumed irreducible in any equational proof of the combined theory. We establish a connection between the equational combination framework and a more algebraic one. A unification algorithm provides a symbolic constraint solver in the combination of algebraic structures whose finite domains of values are non disjoint and correspond to constants. Primal algebras are particular finite algebras of practical relevance for manipulating hardware descriptions.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. F. Baader and K. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. Research Report RR-91-33, DFKI, November 1991. Accepted to CADE-11.

    Google Scholar 

  2. A. Boudet. Unification dans les mélanges de théories équationelles. Application aux axiomes d'associativité, commutativité, identité et idempotence, aux anneaux Booléens, et aux groupes Abéliens. Thèse de Doctorat d'Université, Université de Paris-Sud, Orsay (France), February 1990.

    Google Scholar 

  3. A. Boudet. Unification in a combination of equational theories: An efficient algorithm. In M. E. Stickel, editor, Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany), volume 449 of Lecture Notes in Computer Science. Springer-Verlag, July 1990.

    Google Scholar 

  4. W. Büttner, Unification in finite algebras is unitary. In Proceedings 9th International Conference on Automated Deduction, Argonne (Illinois, USA), pages 368–205. Springer-Verlag, 1988.

    Google Scholar 

  5. W. Büttner, K. Estenfeld, R. Schmid, H.-A. Schneider, and E. Tiden. Symbolic constraint handling through unification in finite algebras. Applicable Algebra in Engineering, Communication and Computation, 1(2):97–118, 1990.

    Google Scholar 

  6. A. Herold. Combination of unification algorithms. In J. Siekmann, editor, Proceedings 8th International Conference on Automated Deduction, Oxford (UK), volume 230 of Lecture Notes in Computer Science, pages 450–469. Springer-Verlag, 1986.

    Google Scholar 

  7. J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: a rule-based survey of unification. In J.-L. Lassez and G. Plotkin, editors, Computational Logic. Essays in honor of Alan Robinson, chapter 8, pages 257–321. MIT Press, Cambridge (MA, USA), 1991.

    Google Scholar 

  8. H. Kirchner and C. Ringeissen. Combining unification problems with constraint solving in finite algebras. Research Report 91-R-106, Centre de Recherche en Informatique de Nancy, 1991.

    Google Scholar 

  9. U. Martin and T. Nipkow. Boolean unification — the story so far. Journal of Symbolic Computation, 7(3 & 4):275–294, 1989. Special issue on unification. Part one.

    Google Scholar 

  10. T. Nipkow. Unification in primal algebras, their powers and their varieties. Journal of the Association for Computing Machinery, 37(1):742–776, October 1990.

    Google Scholar 

  11. C. Ringeissen. Unification in a combination of equational theories with shared constants and its application to primal algebras. Research Report 92-R-061, Centre de Recherche en Informatique de Nancy, 1992.

    Google Scholar 

  12. M. Schmidt-Schauß. Combination of unification algorithms. Journal of Symbolic Computation, 8(1 & 2):51–100, 1989. Special issue on unification. Part two.

    Google Scholar 

  13. E. Tidén. Unification in combinations of collapse-free theories with disjoint sets of functions symbols. In J. Siekmann, editor, Proceedings 8th International Conference on Automated Deduction, Oxford (UK), volume 230 of Lecture Notes in Computer Science, pages 431–449. Springer-Verlag, 1986.

    Google Scholar 

  14. E. Tidén. Symbolic verification of switch-level circuits using a prolog enhanced with unification in finite algebras. In G. Milne, editor, The fusion of hardware design and verification, pages 465–485. IFIP WG 10.2, North-Holland, 1988.

    Google Scholar 

  15. K. Yelick. Unification in combinations of collapse-free regular theories. Journal of Symbolic Computation, 3(1 & 2):153–182, April 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CRIN-CNRS & INRIA-Lorraine, BP 239, 54506, Vandœuvre-lès-Nancy Cedex, France

    Christophe Ringeissen

Authors
  1. Christophe Ringeissen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ringeissen, C. (1992). Unification in a combination of equational theories with shared constants and its application to primal algebras. In: Voronkov, A. (eds) Logic Programming and Automated Reasoning. LPAR 1992. Lecture Notes in Computer Science, vol 624. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013067

Download citation

  • DOI: https://doi.org/10.1007/BFb0013067

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55727-2

  • Online ISBN: 978-3-540-47279-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation