{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T06:52:20Z","timestamp":1649141540099},"reference-count":25,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":3850,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2003,1]]},"DOI":"10.1016\/s0304-3975(02)00583-2","type":"journal-article","created":{"date-parts":[[2002,10,28]],"date-time":"2002-10-28T17:15:47Z","timestamp":1035825347000},"page":"1021-1056","source":"Crossref","is-referenced-by-count":4,"title":["Explicit versus implicit representations of subsets of the Herbrand universe"],"prefix":"10.1016","volume":"290","author":[{"given":"Reinhard","family":"Pichler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(02)00583-2_BIB1","series-title":"Proc. Logics in AI, European Workshop (JELIA\u201990)","first-page":"153","article-title":"Extending resolution for model construction","volume":"vol. 478","author":"Caferra","year":"1991"},{"issue":"2","key":"10.1016\/S0304-3975(02)00583-2_BIB2","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1006\/inco.1994.1056","article-title":"Equational formulae with membership constraints","volume":"112","author":"Comon","year":"1994","journal-title":"Inform. and Comput."},{"issue":"3\/4","key":"10.1016\/S0304-3975(02)00583-2_BIB3","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","article-title":"Equational problems and disunification","volume":"7","author":"Comon","year":"1989","journal-title":"J. Symbolic Comput."},{"issue":"2","key":"10.1016\/S0304-3975(02)00583-2_BIB4","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","article-title":"Hyperresolution and automated model building","volume":"6","author":"Ferm\u00fcller","year":"1996","journal-title":"J. Logic Comput."},{"issue":"1","key":"10.1016\/S0304-3975(02)00583-2_BIB5","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1006\/jsco.1998.0203","article-title":"Negation elimination in empty or permutative theories","volume":"26","author":"Fern\u00e1ndez","year":"1998","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/S0304-3975(02)00583-2_BIB6","doi-asserted-by":"crossref","unstructured":"G. Gottlob, R. Pichler, Working with ARMs: complexity results on atomic representations of Herbrand models, Proc. 14th Ann. IEEE Symp. on Logic in Computer Science (LICS\u201999), Trento, Italy, IEEE Computer Society, Silver Spring, MD, 1999, pp. 306\u2013315.","DOI":"10.1109\/LICS.1999.782625"},{"key":"10.1016\/S0304-3975(02)00583-2_BIB7","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1006\/inco.2000.2915","article-title":"Working with ARMs","volume":"165","author":"Gottlob","year":"2001","journal-title":"Inform. and Comput."},{"issue":"4","key":"10.1016\/S0304-3975(02)00583-2_BIB8","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/BF01893885","article-title":"Sufficient-completeness, ground-reducibility and their complexity","volume":"28","author":"Kapur","year":"1991","journal-title":"Acta Inform."},{"key":"10.1016\/S0304-3975(02)00583-2_BIB9","series-title":"Proc. 4th Internat. Conf. on Logic Programming (ICLP\u201987), Melbourne, Victoria, Australia","first-page":"219","article-title":"Answer sets and negation as failure","author":"Kunen","year":"1987"},{"key":"10.1016\/S0304-3975(02)00583-2_BIB10","doi-asserted-by":"crossref","unstructured":"G. Kuper, K. McAloon, K. Palem, K. Perry, Efficient parallel algorithms for anti-unification and relative complement, Proc. 3rd Ann. Symp. on Logic in Computer Science (LICS\u201988), Edinburgh, Scotland, UK, IEEE Computer Society, Silver Spring, MD, 1988, pp. 112\u2013120.","DOI":"10.1109\/LICS.1988.5109"},{"key":"10.1016\/S0304-3975(02)00583-2_BIB11","doi-asserted-by":"crossref","unstructured":"J.-L. Lassez, M. Maher, K. Marriott, Unification revisited, in: M. Boscarol, L. Carlucci Aielli, G. Levi (Eds.), Proc. Workshop on Foundations of Logic and Functional Programming, Lecture Notes in Computer Science, vol. 306, Trento, Italy, Springer, Berlin, 1986, pp. 67\u2013113.","DOI":"10.1007\/3-540-19129-1_4"},{"key":"10.1016\/S0304-3975(02)00583-2_BIB12","doi-asserted-by":"crossref","unstructured":"J.-L. Lassez, M. Maher, K. Marriott, Elimination of negation in term algebras, in: A. Tarlecki (Ed.), Proc. 16th Internat. Symp. on Mathematical Foundations of Computer Science (MFCS\u201991), Lecture Notes in Computer Science, vol. 520, Kazimierz Dolny, Poland, Springer, Berlin, 1991, pp. 1\u201316.","DOI":"10.1007\/3-540-54345-7_44"},{"issue":"3","key":"10.1016\/S0304-3975(02)00583-2_BIB13","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/BF00243794","article-title":"Explicit representation of terms defined by counter examples","volume":"3","author":"Lassez","year":"1987","journal-title":"J. Automat. Reason."},{"key":"10.1016\/S0304-3975(02)00583-2_BIB14","doi-asserted-by":"crossref","unstructured":"M. Maher, Complete axiomatizations of the algebras of finite, rational and infinite trees, Proc. 3rd Ann. Symp. on Logic in Computer Science (LICS\u201988), Edinburgh, Scotland, UK, IEEE Computer Society, Silver Spring, MD, 1988, pp. 348\u2013357.","DOI":"10.1109\/LICS.1988.5132"},{"issue":"2","key":"10.1016\/S0304-3975(02)00583-2_BIB15","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BF01534454","article-title":"On inductive inference of cyclic structures","volume":"15","author":"Maher","year":"1995","journal-title":"Ann. Math. Artificial Intelligence"},{"key":"10.1016\/S0304-3975(02)00583-2_BIB16","unstructured":"K. Marriott, Finding explicit representations for subsets of the Herbrand Universe, Ph.D. thesis, University of Melbourne, Australia, 1988."},{"issue":"2","key":"10.1016\/S0304-3975(02)00583-2_BIB17","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","article-title":"An efficient unification algorithm","volume":"4","author":"Martelli","year":"1982","journal-title":"ACM Trans. Programming Languages and Systems"},{"key":"10.1016\/S0304-3975(02)00583-2_BIB18","doi-asserted-by":"crossref","unstructured":"R. Pichler, Solving equational problems efficiently, in: H. Ganzinger (Ed.), Proc. 16th Internat. Conf. on Automated Deduction (CADE-16), Lecture Notes in Artificial Intelligence, vol. 1632, Trento, Italy, Springer, Berlin, 1999, pp. 97\u2013111.","DOI":"10.1007\/3-540-48660-7_7"},{"key":"10.1016\/S0304-3975(02)00583-2_BIB19","doi-asserted-by":"crossref","unstructured":"R. Pichler, The explicit representability of implicit generalizations, in: L. Bachmai (Ed.), Proc. 11th Internat. Conf. on Rewriting Techniques and Applications (RTA 2000), Lecture Notes in Computer Science, vol. 1833, Norwich, UK, Springer, Berlin, 2000, pp. 187\u2013202.","DOI":"10.1007\/10721975_13"},{"key":"10.1016\/S0304-3975(02)00583-2_BIB20","doi-asserted-by":"crossref","unstructured":"R. Pichler, Negation elimination from simple equational formulae, in: U. Montanari, J.D.P. Rolim, E. Welzl (Eds.), Proc. 27th Internat. Coll. on Automata, Languages and Programming (ICALP 2000), Lecture Notes in Computer Science, vol. 1553, Geneva, Switzerland, Springer, Berlin, 2000, pp. 612\u2013623.","DOI":"10.1007\/3-540-45022-X_52"},{"key":"10.1016\/S0304-3975(02)00583-2_BIB21","unstructured":"M. Rusinowitch, C. Kirchner, H. Kirchner, Deduction with symbolic constraints. Revue Fran\u00e7aise d'Intelligence Artificielle 4 (3) (1990) 9\u201352 (Special issue on Automatic Deduction)."},{"key":"10.1016\/S0304-3975(02)00583-2_BIB22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","article-title":"The polynomial time hierarchy","volume":"3","author":"Stockmeyer","year":"1976","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(02)00583-2_BIB23","doi-asserted-by":"crossref","unstructured":"M. Tajine, The negation elimination from syntactic equational formulas is decidable, in: C. Kirchner (Ed.), Proc. 5th Internat. Conf. on Rewriting Techniques and Applications (RTA\u201993), Lecture Notes in Computer Science, vol. 690, Montreal, Canada, Springer, Berlin, 1993, pp. 316\u2013327.","DOI":"10.1007\/3-540-56868-9_24"},{"key":"10.1016\/S0304-3975(02)00583-2_BIB24","doi-asserted-by":"crossref","unstructured":"J.-J. Thiel, Stop losing sleep over incomplete data type specifications, Proc. 11th Ann. ACM Symp. on Principles of Programming Languages (POPL\u201984), Salt Lake City, Utah, ACM Press, New York, 1984, pp. 76\u201382.","DOI":"10.1145\/800017.800518"},{"key":"10.1016\/S0304-3975(02)00583-2_BIB25","doi-asserted-by":"crossref","unstructured":"S. Vorobyov, An improved lower bound for the elementary theories of trees, in: M.A. McRobbie, K. Slaney (Eds.), Proc. 13th Internat. Conf. on Automated Deduction (CADE-13), Lecture Notes in Artificial Intelligence, vol. 690, New Brunswick, NJ, USA, Springer, Berlin, 1996, pp. 316\u2013327.","DOI":"10.1007\/3-540-61511-3_91"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397502005832?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397502005832?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T19:30:11Z","timestamp":1554406211000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397502005832"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,1]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,1]]}},"alternative-id":["S0304397502005832"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(02)00583-2","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2003,1]]}}}