{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:58:30Z","timestamp":1725494310324},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_11","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T15:53:07Z","timestamp":1194623587000},"page":"157-171","source":"Crossref","is-referenced-by-count":3,"title":["On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results"],"prefix":"10.1007","author":[{"given":"Viorica","family":"Sofronie-Stokkermans","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"11_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/3-540-54317-1_89","volume-title":"Proc. 2nd International Workshop on Conditional and Typed Rewriting","author":"L. Bachmair","year":"1991","unstructured":"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\u2013180, Berlin, 1991. Springer-Verlag."},{"issue":"6","key":"11_CR2","doi-asserted-by":"publisher","first-page":"1007","DOI":"10.1145\/293347.293352","volume":"45","author":"L. Bachmair","year":"1998","unstructured":"L. Bachmair and H. Ganzinger. Ordered chaining calculi for first-order theories of transitive relations. Journal of the ACM,45(6):1007\u20131049, 1998.","journal-title":"Journal of the ACM"},{"key":"11_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/BFb0022557","volume-title":"Computational Logic and Proof Theory, 3rd Kurt G\u00f6del Colloquium","author":"L. Bachmair","year":"1993","unstructured":"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\u00f6del Colloquium, LNCS 713, pages 83\u201396. Springer Verlag, 1993."},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"S. Burris and R. McKenzie. Decidability and Boolean Representations. Memoirs of the AMS, Volume 32, Number 246. American Mathematical Society, 1981.","DOI":"10.1090\/memo\/0246"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"S. Burris and H.P. Sankappanavar. A Course in Universal Algebra. Graduate Texts in Mathematics. Springer, 1981.","DOI":"10.1007\/978-1-4613-8130-3"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"S.S. Cosmadakis. Equational Theories and Database Constraints. PhD thesis, Massachusetts Institute of Technology, 1985.","DOI":"10.1145\/22145.22176"},{"key":"11_CR7","unstructured":"B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990."},{"key":"11_CR8","unstructured":"H. Ganzinger, U. Hustadt, C. Meyer, and R. Schmidt. A resolution-based decision procedure for extensions of K4. Proceedings of AIML\u201998, 1999. To appear."},{"issue":"3","key":"11_CR9","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/0168-0072(89)90032-8","volume":"44","author":"R. Goldblatt","year":"1989","unstructured":"R. Goldblatt. Varieties of complex algebras. Annals of Pure and Applied Logic, 44(3):153\u2013301, 1989.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1","key":"11_CR10","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1137\/0216011","volume":"16","author":"H.B. Hunt","year":"1987","unstructured":"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\u2013148, 1987.","journal-title":"SIAM Journal of Computation"},{"issue":"74","key":"11_CR11","doi-asserted-by":"publisher","first-page":"891","DOI":"10.2307\/2372123","volume":"73","author":"B. J\u00f3nsson","year":"1951","unstructured":"B. J\u00f3nsson and A. Tarski. Boolean algebras with operators, Part I & II. American Journal of Mathematics, 73 & 74:891\u2013939 & 127-162, 1951 & 1952.","journal-title":"American Journal of Mathematics"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"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\u2013151. IEEE Computer Society Press, 1996.","DOI":"10.1109\/LICS.1996.561313"},{"issue":"3","key":"11_CR13","doi-asserted-by":"publisher","first-page":"61","DOI":"10.2307\/2268172","volume":"8","author":"J.C.C. McKinsey","year":"1943","unstructured":"J.C.C. McKinsey. The decision problem for some classes of sentences without quantifiers. The Journal of Symbolic Logic, 8(3):61\u201376, 1943.","journal-title":"The Journal of Symbolic Logic"},{"key":"11_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"589","DOI":"10.1007\/BFb0055809","volume-title":"Proceedings of MFCS\u201998","author":"P. Mielniczuk","year":"1998","unstructured":"P. Mielniczuk and L. Pacholski. Tarskian set constraints are in NEXPTIME. In Lubos Prim et. al., editor, Proceedings of MFCS\u201998, LNCS 1450, pages 589\u2013596. Springer Verlag, 1998."},{"key":"11_CR15","first-page":"39","volume":"23","author":"H. Priestley","year":"1984","unstructured":"H. Priestley. Ordered sets and duality for distributive lattices. Annals of Discrete Mathematics, 23:39\u201360, 1984.","journal-title":"Annals of Discrete Mathematics"},{"key":"11_CR16","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1112\/blms\/2.2.186","volume":"2","author":"H.A. Priestley","year":"1970","unstructured":"H.A. Priestley. Representation of distributive lattices by means of ordered Stone spaces. Bull. London Math. Soc., 2:186\u2013190, 1970.","journal-title":"Bull. London Math. Soc."},{"key":"11_CR17","first-page":"1","volume":"4","author":"T. Skolem","year":"1920","unstructured":"T. Skolem. Logisch-kombinatorische Untersuchungen \u00fcber die Erf\u00fcllbarkeit und Beweisbarkeit mathematischen S\u00e4tze nebst einem Theoreme \u00fcber dichte Mengen. Videnskapsselskapets skrifter I, Matematisk-naturvidenskabelig klasse, Videnskab-sakademiet i Kristiania, 4:1\u201336, 1920. Also in T. Skolem, Select Works in Logic, Scandinavian University Books, Oslo, 1970, pp.103-136.","journal-title":"Videnskapsselskapets skrifter I, Matematisk-naturvidenskabelig klasse, Videnskab-sakademiet i Kristiania"},{"key":"11_CR18","volume-title":"Fibered Structures and Applications to Automated Theorem Proving in Certain Classes of Finitely-Valued Logics and to Modeling Interacting Systems","author":"V. Sofronie-Stokkermans","year":"1997","unstructured":"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."},{"key":"11_CR19","unstructured":"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."},{"key":"11_CR20","unstructured":"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."},{"key":"11_CR21","volume-title":"Canonical Transformations in Algebra, Universal Algebra, and Logic","author":"G. Struth","year":"1998","unstructured":"G. Struth. Canonical Transformations in Algebra, Universal Algebra, and Logic. PhD thesis, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, 1998."},{"key":"11_CR22","first-page":"115","volume-title":"Seminars in Mathematics V.A. SteklovMath. Inst., Leningrad","author":"G. S. Tseitin","year":"1970","unstructured":"G. S. Tseitin. On the complexity of derivation in propositional calculus. In Seminars in Mathematics V.A. SteklovMath. Inst., Leningrad, volume 8, pages 115\u2013125. Consultants Bureau, New York-London, 1970. Reprinted in J. Siekmann and G. Wrightson (eds): Automation of Reasoning, Vol. 2, 1983, Springer, pp.466-486."},{"key":"11_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-61511-3_75","volume-title":"Proceedings of CADE-13","author":"Ch. Weidenbach","year":"1996","unstructured":"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\u2013145. Springer Verlag, 1996."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T04:56:29Z","timestamp":1556945789000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}