{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T13:23:07Z","timestamp":1760707387330,"version":"3.41.0"},"reference-count":13,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2004,7,1]],"date-time":"2004-07-01T00:00:00Z","timestamp":1088640000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2004,7]]},"abstract":"\n We present a decision algorithm for the problem\n Val<\/jats:italic>\n (\n FT<\/jats:italic>\n ) of deciding validity of first-order sentences in the theory of feature trees. Its time complexity is exp\n \u230ac\u00b7m\u230b<\/jats:sub>\n (\n c<\/jats:italic>\n \u00b7\n n<\/jats:italic>\n ) where\n n<\/jats:italic>\n is the length of a sentence,\n m<\/jats:italic>\n is the quantifier depth of a sequence, and\n c<\/jats:italic>\n is a constant. The function exp\n \n i<\/jats:italic>\n <\/jats:sub>\n (\n j<\/jats:italic>\n ) is an exponential tower of 2's of height\n i<\/jats:italic>\n , to power\n j<\/jats:italic>\n (exp\n 0<\/jats:sub>\n (\n j<\/jats:italic>\n ) =\n j<\/jats:italic>\n and exp\n \n i<\/jats:italic>\n +1\n <\/jats:sub>\n (\n j<\/jats:italic>\n ) = 2\n \n exp\n \n i<\/jats:italic>\n <\/jats:sub>\n (\n j<\/jats:italic>\n )\n <\/jats:sup>\n ). Moreover we prove that the presented algorithm is optimal, deriving a lower bound which matches the upper one.\n <\/jats:p>","DOI":"10.1145\/1013560.1013561","type":"journal-article","created":{"date-parts":[[2004,10,7]],"date-time":"2004-10-07T17:38:56Z","timestamp":1097170736000},"page":"385-402","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Basic theory of feature trees"],"prefix":"10.1145","volume":"5","author":[{"given":"Pawel","family":"Mielniczuk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2004,7]]},"reference":[{"volume-title":"Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning. 1--18","author":"Ait-Kaci H.","key":"e_1_2_1_1_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90209-7"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/0743-1066(95)00033-G","article-title":"A complete axiomatization of a theory with feature and arity constraints","volume":"24","author":"Backofen R.","year":"1995","journal-title":"J. Logic Program."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00188-O"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Backofen R. and Treinen R. 1994. How to win a game with features. In Constraints in Computational Logics'94. Vol. 845. Springer-Verlag Berlin Germany 320--335. Backofen R. and Treinen R. 1994. How to win a game with features. In Constraints in Computational Logics'94. Vol. 845. Springer-Verlag Berlin Germany 320--335.","DOI":"10.1007\/BFb0016863"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0168-0072(90)90080-L","article-title":"A uniform method for proving lower bounds on the computational complexity of logical theories","volume":"48","author":"Compton K. J.","year":"1990","journal-title":"Ann. Pure Appl. Logic"},{"key":"e_1_2_1_7_1","first-page":"27","article-title":"Super-exponential complexity of presburger arithmetic","volume":"7","author":"Fischer M. J.","year":"1974","journal-title":"SIAM-AMS Proceedings."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","article-title":"Constraint logic programming: A survey","volume":"19","author":"Jaffar J.","year":"1994","journal-title":"J. Logic Program."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2878"},{"volume":"1330","volume-title":"Proceedings of the Third International Conference on Constraint Programming. Lecture Notes in Computer Science","author":"Mueller M.","key":"e_1_2_1_10_1"},{"volume-title":"LICS'98","author":"Mueller M.","key":"e_1_2_1_11_1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/0743-1066(94)90044-2","article-title":"Records for logic programming","volume":"18","author":"Smolka G.","year":"1994","journal-title":"J. Logic Program."},{"volume-title":"Thirteenth International Conference on Automated Deduction","series-title":"Lecture Notes in Computer Science","author":"Vorobyov S.","key":"e_1_2_1_13_1"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1013560.1013561","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1013560.1013561","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:19:03Z","timestamp":1750263543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1013560.1013561"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,7]]},"references-count":13,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2004,7]]}},"alternative-id":["10.1145\/1013560.1013561"],"URL":"https:\/\/doi.org\/10.1145\/1013560.1013561","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2004,7]]},"assertion":[{"value":"2004-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}