Skip to main content
SpringerLink
Log in

A New Correctness Proof of the Nelson-Oppen Combination Procedure

  • Chapter
Frontiers of Combining Systems

Part of the book series: Applied Logic Series ((APLS,volume 3))

Abstract

The Nelson-Oppen combination procedure, which combines satisfiability procedures for a class of first-order theories by propagation of equalities between variables, is one of the most general combination methods in the field of theory combination. We describe a new non- deterministic version of the procedure that has been used to extend the Constraint Logic Programming Scheme to unions of constraint theories. The correctness proof of the procedure that we give in this paper not only constitutes a novel and easier proof of Nelson and Oppen’s original results, but also shows that equality sharing between the satisfiability procedures of the component theories, the main idea of the method, can be confined to a restricted set of variables.

While working on the new correctness proof, we also found a new characterization of the consistency of the union of first-order theories. We discuss and give a proof of such characterization as well.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Franz Baader, July 1995. Personal communication

    Google Scholar 

  • Franz Baader and Klaus U. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In Proceedings of the 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 50–65. Springer-Verlag, 1992

    Google Scholar 

  • Franz Baader and Klaus U. Schulz. Combination of constraint solving techniques: An algebraic point of view. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Computer Science, pages 50–65. Springer-Verlag, 1995

    Google Scholar 

  • Franz Baader and Klaus U. Schulz. Combination techniques and decision problems for disunification. Theoretical Computer Science, 142:229–255, 1995

    Article  MATH  MathSciNet  Google Scholar 

  • Franz Baader and Klaus U. Schulz. On the combination of symbolic constraints, solution domains, and constraint solvers. In Proceedings of the First International Conference on Principles and Practice of Constraint Programming, Cassis (France), September 1995

    Google Scholar 

  • Alexandre Boudet. Unification in a combination of equational theories: An efficient algorithm. In M. E. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1990

    Google Scholar 

  • Alexandre Boudet. Combining unification algorithms. Journal of Symbolic Computation, 16(6):597–626, December 1993

    Article  MATH  MathSciNet  Google Scholar 

  • C. C. Chang and H. Jerome Keisler. Model Theory, volume 73 of Studies in logic and the foundations of mathematics. North-Holland, Amsterdam-New York-Oxford-Tokyo, 1990

    Book  MATH  Google Scholar 

  • E. Domenjoud, F. Klay, and C. Ringeissen. Combination techniques for non-disjoint equational theories. In A. Bundy, editor, Proceedings 12th International Conference on Automated Deduction, Nancy (France), volume 814 of Lecture Notes in Artificial Intelligence, pages 267–281. Springer-Verlag, 1994

    Google Scholar 

  • 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 Artificial Intelligence, pages 450–469. Springer-Verlag, 1986

    Google Scholar 

  • Joxan Jaffar and Jean-Louis Lassez. Constraint Logic Programming. Technical Report 86/74, Monash University, Victoria, Australia, June 1986

    Google Scholar 

  • Joxan Jaffar and Jean-Louis Lassez. Constraint Logic Programming. In POPL’87: Proceedings 14th ACM Symposium on Principles of Programming Languages, pages 111–119, Munich, January 1987. ACM

    Google Scholar 

  • Joxan Jaffar and Michael Maher. Constraint Logic Programming: A Survey. Journal of Logic Programming, 19/20:503–581,1994

    Article  MathSciNet  Google Scholar 

  • HĂ©lène Kirchner and Christophe Ringeissen. A constraint solver in finite algebras and its combination with unification algorithms. In K. Apt, editor, Proc. Joint International Conference and Symposium on Logic Programming, pages 225–239. MIT Press, 1992

    Google Scholar 

  • HĂ©lène Kirchner and Christophe Ringeissen. Constraint solving by narrowing in combined algebraic domains. In P. Van Hentenryck, editor, Proc. 11th International Conference on Logic Programming, pages 617–631. The MIT press, 1994

    Google Scholar 

  • Greg Nelson. Combining satisfiability procedures by equality-sharing. Contemporary Mathematics, 29:201–211,1984

    Article  Google Scholar 

  • Greg Nelson and Derek C. Oppen. Simplification by cooperating decision procedures. ACM Trans, on Programming Languages and Systems, l(2):245–257, October 1979

    Article  MATH  Google Scholar 

  • Derek C. Oppen. Complexity, convexity and combinations of theories. Theoretical Computer Science, 12, 1980

    Google Scholar 

  • Christophe Ringeissen. Unification in a combination of equational theories with shared constants and its application to primal algebras. In Proceedings of the 1st International Conference on Logic Programming and Automated Reasoning, volume 624 of Lecture Notes in Artificial Intelligence, pages 261–272. Springer-Verlag, 1992

    Chapter  Google Scholar 

  • Manfred Schmidt-Schaufβ. Unification in a combination of disjoint equational theories. In Proceedings of the 9th International Conference on Automated Deduction, volume 310 of Lecture Notes in Computer Science, pages 378–396. Springer-Verlag, 1988

    Chapter  Google Scholar 

  • Manfred Schmidt-Schaufβ. Combination of unification algorithms. Journal of Symbolic Computation, 8(1–2):51–100,1989

    Article  MathSciNet  Google Scholar 

  • Joseph. R. Shoenfield. Mathematical Logic. Addison-Wesley, Reading, MA, 1967

    Google Scholar 

  • Robert E. Shostak. A practical decision procedure for arithmetic with function symbols. Journal of the ACM, 26(2):351–360, April 1979

    Article  MATH  MathSciNet  Google Scholar 

  • Robert E. Shostak. Deciding combinations of theories. Journal of the ACM, 31:1–12, 1984

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  • Cesare Tinelli. Extending the CLP scheme to unions of constraint theories. Master’s thesis, Department of Computer Science, University of Illinois, Urbana-Champaign, Illinois, October 1995

    Google Scholar 

  • K. Yelik. Combining unification algorithms for confined equational theories. Journal of Symbolic Computation, 3(1), April 1987

    Article  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Illinois at Urbana-Champaign, USA

    Cesare Tinelli & Mehdi Harandi

Authors
  1. Cesare Tinelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mehdi Harandi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LuFG Theoretical Computer Science, Technical University of Aachen, Germany

    Frans Baader

  2. CIS, University of Munich, Germany

    Klaus U. Schulz

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer Science+Business Media New York

About this chapter

Cite this chapter

Tinelli, C., Harandi, M. (1996). A New Correctness Proof of the Nelson-Oppen Combination Procedure. In: Baader, F., Schulz, K.U. (eds) Frontiers of Combining Systems. Applied Logic Series, vol 3. Springer, Dordrecht. https://doi.org/10.1007/978-94-009-0349-4_5

Download citation

  • DOI: https://doi.org/10.1007/978-94-009-0349-4_5

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-94-010-6643-3

  • Online ISBN: 978-94-009-0349-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation