*********************************** *********************************** From Ralph Freese (ralph@math.hawaii.edu) July 1 ... Not long ago we discovered that the quasi word problem (ususually just called the word problem) had be solved in 1920 by Thoralf Skolem. It appeared in the first ref below which is hard to find but it is reprinted in the second. @ARTICLE{Skolem1920, AUTHOR = {T. Skolem}, TITLE = {Logisch-kombinatorische {U}ntersuchungen \"uber die {E}rf\"ullbarkeit und {B}eweisbarkeit mathematischen {S}\"atze nebst einem {T}heoreme \"uber dichte {M}engen}, JOURNAL = {Videnskapsselskapets skrifter I, Matematisk-naturvidenskabelig klasse, Videnskabsakademiet i Kristiania}, VOLUME = {4}, YEAR = {1920}, PAGES = {1--36}, } @BOOK{Skolem1970, AUTHOR = {T. Skolem}, TITLE = {Select Works in Logic}, PUBLISHER = {Scandinavian University Books}, ADDRESS = {Oslo}, YEAR = {1970}, } What is interesting is that his solution is polynomial time. Later solutions in the 40's and 50's where exponential. We have a book on free lattices which gives the interesting history of this: @BOOK{FreeseJezekNation1995, AUTHOR = {Ralph Freese and Jaroslav {Je\v zek} and J. B. Nation}, TITLE = {Free Lattices}, PUBLISHER = {Amer. Math. Soc.}, ADDRESS = {Providence}, YEAR = {1995}, NOTE = {Mathematical Surveys and Monographs, vol. 42}, } This book gives a quadratic algorithm for the word problem for free lattices and can be modified to work for finitely presented lattices, i.e., for the quasi word problem. Ralph ****************************************** ****************************************** From Phokion Kolaitis July 8 David, Thanks for your message and the references. Here is another relevant reference, which extends Skolem's result. Best, Phokion ------------- >From MELVYL@UCCMVSA.UCOP.EDU Tue Jul 8 09:42:18 1997 Return-Path: Received: from uccmvsa.ucop.edu (uccmvsa.ucop.edu [128.48.140.3]) by lorraine.loria.fr (8.8.5/8.8.5/8.8.5/JCG) with SMTP id JAA18168 for ; Tue, 8 Jul 1997 09:42:15 +0200 (MET DST) Message-Id: <199707080742.JAA18168@lorraine.loria.fr> Received: from UCCMVSA.UCOP.EDU by uccmvsa.ucop.edu (IBM MVS SMTP V3R1) with BSMTP id 7871; Tue, 08 Jul 97 00:42:15 PDT Received: by UCCMVSA.UCOP.EDU Tue, 08 Jul 97 00:42:07 PDT Date: Tue, 08 Jul 97 00:42:07 PDT From: Melvyl System To: kolaitis@loria.fr Subject: (id: HWE92111) MELVYL system mail result Status: R Search request: FIND PA BURRIS, S Search result: 4 citations in the INSPEC database Display: D ABS 1 1. Burris, S. Polynomial time uniform word problems. Mathematical Logic Quarterly, 1995, vol.41, (no.2):173-82. Pub type: Theoretical or Mathematical. Abstract: We have two polynomial time results for the uniform word problem for a quasivariety Q: (a) The uniform word problem for Q can be solved in polynomial time iff one can find a certain congruence on finite partial algebras in polynomial time. (b) Let Q* be the relational class determined by Q. If any universal Horn class between the universal closure S(Q*) and the weak embedding closure S(Q*) of Q* is finitely axiomatizable then the uniform word problem for Q is solvable in polynomial time. This covers Skolem's 1920 solution to the uniform word problem for lattices and Evans' 1953 applications of the weak embeddability property for finite partial V algebras. ****************************************** ****************************************** From: Sergei Vorobyov , July 8 Dear David, Here are the notes I promised you. 1. R.Statman's paper I mentioned is: Complexity of derivations from quentifier-free Horn formulae, mechanical introduction of explicit definitions, and refinement of completeness theorems. Logic Colloquium'76, R.Gandy, M.Hyland, eds, North-Holl Pub Co, 1977, pp. 505--518. See also Statman's paper in the Handbook of Mathematical Logic, 1977 2. In relation to Immermann-Vardi's theorem, Larry Stockmeyer in @ARTICLE{Stockmeyer87, author = {Stockmeyer, L.}, title = {Classifying the computational complexity of problems}, year = 1987, journal = {Journal of Symbolic Logic}, volume = {52}, number = {1}, pages = {1--43} } mentions also (second half of section 7.3, pp 33--34) the results of Yu. Gurevich and A. Livchak (a former student of Gurevich) on logics capturing PTIME. 3. The relevant references about quasi-word pbms are also @ARTICLE{Cosmadakis88, AUTHOR = {Cosmadakis, S. S.}, TITLE = {The Word and Generator Problems for Lattices}, YEAR = {1988}, JOURNAL = {Information \& Computation}, VOLUME = {77} } @ARTICLE{CosmadakisKanellakisVardi90, AUTHOR = {Cosmadakis, S. S. and Kanellakis, P. C. and Vardi, M. Y.}, TITLE = {Polynomial-Time Implication Problems for Unary Inclusion Dependencies}, YEAR = {1990}, JOURNAL = {Journal of the ACM}, VOLUME = {37} } 4. Phokion Kolaitis mentioned the name of Stanley Burris in connection with the decidability of lattice quasi-word problems. I found two references @BOOK{BurrisMcKenzie81, AUTHOR = {Burris, Stanley and McKenzie, Ralph}, TITLE = {Decidability and Boolean representations}, PUBLISHER = {American Mathematical Society}, ADDRESS = {Providence, RI}, YEAR = {1981}, SERIES = {Memoirs of the American Mathematical Society series}, VOLUME = {32/246} } @BOOK{BurrisSankappanavar81, AUTHOR = {Burris, Stanley and Sankappanavar, H.P.}, TITLE = {A course in universal algebra}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1981}, SERIES = {Graduate Texts in Mathematics}, VOLUME = {78} } 5. In his talk at LICS97 Kobayashi considered a type system for communicating processes with a polynomial decision problem. I wonder if you could get it for free from the locality analysis (as far as I remember, he improved his results and refered to a subsequent paper written after the LICS submission). 6. The proof of completeness by saturation you gave in your talk very much resembles the one from AUTHOR = {Chang, Chin-Liang and Lee, Richard Char-Tung}, TITLE = {Symbolic Logic and Mechanical Theorem Proving}, PUBLISHER = {Academic Press}, ADDRESS = {New York;London}, YEAR = {1973}, SERIES = {Computer Science and Applied Mathematics} } Section 7.5, pp. 142--145 (you'll also find references for the authorship there) and (for me) very much like the standard proof of Goedel's completeness theorem as I remember it.