Skip to main content
SpringerLink
Log in

On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results

  • Conference paper
  • First Online:
Automated Deduction — CADE-16 (CADE 1999)

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

Included in the following conference series:

Abstract

In this paper we establish a link between satisfiability of universal sentences with respect to varieties of distributive lattices with operators and satisfiability with respect to certain classes of relational structures. We use these results for giving a method for translation to clause form of universal sentences in such varieties, and then use results from automated theorem proving to obtain decidability and complexity results for the universal theory of some such varieties.

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

  1. L. Bachmair and H. Ganzinger. Completion of first-order clauses with equality by strict superposition. In St. Kaplan and M. Okada, editors, Proc. 2nd International Workshop on Conditional and Typed Rewriting, Montreal, LNCS 516, pages 162–180, Berlin, 1991. Springer-Verlag.

    Google Scholar 

  2. L. Bachmair and H. Ganzinger. Ordered chaining calculi for first-order theories of transitive relations. Journal of the ACM,45(6):1007–1049, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  3. L. Bachmair, H. Ganzinger, and U. Waldmann. Superposition with simplification as a decision procedure for the monadic class with equality. In G. Gottlob, A. Leitsch, and D. Mundici, editors, Computational Logic and Proof Theory, 3rd Kurt Gödel Colloquium, LNCS 713, pages 83–96. Springer Verlag, 1993.

    Google Scholar 

  4. S. Burris and R. McKenzie. Decidability and Boolean Representations. Memoirs of the AMS, Volume 32, Number 246. American Mathematical Society, 1981.

    Google Scholar 

  5. S. Burris and H.P. Sankappanavar. A Course in Universal Algebra. Graduate Texts in Mathematics. Springer, 1981.

    Google Scholar 

  6. S.S. Cosmadakis. Equational Theories and Database Constraints. PhD thesis, Massachusetts Institute of Technology, 1985.

    Google Scholar 

  7. B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.

    Google Scholar 

  8. H. Ganzinger, U. Hustadt, C. Meyer, and R. Schmidt. A resolution-based decision procedure for extensions of K4. Proceedings of AIML’98, 1999. To appear.

    Google Scholar 

  9. R. Goldblatt. Varieties of complex algebras. Annals of Pure and Applied Logic, 44(3):153–301, 1989.

    Article  MathSciNet  Google Scholar 

  10. H.B. Hunt, D.J. Rosenkrantz, and P.A. Bloniarz. On the computational complexity of algebra of lattices. SIAM Journal of Computation, 16(1):129–148, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  11. B. Jónsson and A. Tarski. Boolean algebras with operators, Part I & II. American Journal of Mathematics, 73 & 74:891–939 & 127-162, 1951 & 1952.

    Article  MATH  MathSciNet  Google Scholar 

  12. D. McAllester, R. Givan, D. Kozen, and C. Witty. Tarskian set constraints. In Proceedings of the Eleventh Annual IEEE Symposium on Logic In Computer Science, pages 138–151. IEEE Computer Society Press, 1996.

    Google Scholar 

  13. J.C.C. McKinsey. The decision problem for some classes of sentences without quantifiers. The Journal of Symbolic Logic, 8(3):61–76, 1943.

    Article  MATH  MathSciNet  Google Scholar 

  14. P. Mielniczuk and L. Pacholski. Tarskian set constraints are in NEXPTIME. In Lubos Prim et. al., editor, Proceedings of MFCS’98, LNCS 1450, pages 589–596. Springer Verlag, 1998.

    Google Scholar 

  15. H. Priestley. Ordered sets and duality for distributive lattices. Annals of Discrete Mathematics, 23:39–60, 1984.

    MathSciNet  Google Scholar 

  16. H.A. Priestley. Representation of distributive lattices by means of ordered Stone spaces. Bull. London Math. Soc., 2:186–190, 1970.

    Article  MATH  MathSciNet  Google Scholar 

  17. T. Skolem. Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit und Beweisbarkeit mathematischen Sätze nebst einem Theoreme über dichte Mengen. Videnskapsselskapets skrifter I, Matematisk-naturvidenskabelig klasse, Videnskab-sakademiet i Kristiania, 4:1–36, 1920. Also in T. Skolem, Select Works in Logic, Scandinavian University Books, Oslo, 1970, pp.103-136.

    Google Scholar 

  18. V. Sofronie-Stokkermans. Fibered Structures and Applications to Automated Theorem Proving in Certain Classes of Finitely-Valued Logics and to Modeling Interacting Systems. PhD thesis, RISC-Linz, J.Kepler University Linz, Austria, 1997.

    Google Scholar 

  19. V. Sofronie-Stokkermans. Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of non-classical logics I, II. Studia Logica, 1999. To appear.

    Google Scholar 

  20. V. Sofronie-Stokkermans. Representation theorems and theorem proving in nonclassical logics. In Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic. IEEE Computer Sociaty Press, 1999. To appear.

    Google Scholar 

  21. G. Struth. Canonical Transformations in Algebra, Universal Algebra, and Logic. PhD thesis, Max-Planck-Institut für Informatik, Saarbrücken, 1998.

    Google Scholar 

  22. G. S. Tseitin. On the complexity of derivation in propositional calculus. In Seminars in Mathematics V.A. SteklovMath. Inst., Leningrad, volume 8, pages 115–125. Consultants Bureau, New York-London, 1970. Reprinted in J. Siekmann and G. Wrightson (eds): Automation of Reasoning, Vol. 2, 1983, Springer, pp.466-486.

    Google Scholar 

  23. Ch. Weidenbach, B. Gaede, and G. Rock. SPASS & FLOTTER Version 0.42. In M.A. McRobie and J.K. Slaney, editors, Proceedings of CADE-13, LNCS 1104, pages 141–145. Springer Verlag, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Max-Planck-Institut für Informatik, Im Stadtwald, D-66123, Saarbrücken, Germany

    Viorica Sofronie-Stokkermans

Authors
  1. Viorica Sofronie-Stokkermans
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sofronie-Stokkermans, V. (1999). On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results. In: Automated Deduction — CADE-16. CADE 1999. Lecture Notes in Computer Science(), vol 1632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48660-7_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-48660-7_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66222-8

  • Online ISBN: 978-3-540-48660-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation