{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:22:22Z","timestamp":1725495742251},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677154"},{"type":"electronic","value":"9783540450221"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-45022-x_52","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T23:57:25Z","timestamp":1194998245000},"page":"612-623","source":"Crossref","is-referenced-by-count":1,"title":["Negation Elimination from Simple Equational Formulae"],"prefix":"10.1007","author":[{"given":"Reinhard","family":"Pichler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,2,18]]},"reference":[{"key":"52_CR1","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1994.1056","volume":"112","author":"H. Comon","year":"1994","unstructured":"H. Comon, C. Delor: Equational Formulae with Membership Constraints, Journal of Information and Computation, Vol 112, pp. 167\u2013216 (1994).","journal-title":"Journal of Information and Computation"},{"key":"52_CR2","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H. Comon","year":"1989","unstructured":"H. Comon, P. Lescanne: Equational Problems and Disunification, Journal of Symbolic Computation, Vol 7, pp. 371\u2013425 (1989).","journal-title":"Journal of Symbolic Computation"},{"key":"52_CR3","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1006\/jsco.1998.0203","volume":"26","author":"M. Fern\u00e1ndez","year":"1998","unstructured":"M. Fern\u00e1ndez: Negation Elimination in Empty or Permutative Theories, Journal of Symbolic Computation, Vol 26, pp. 97\u2013133 (1998).","journal-title":"Journal of Symbolic Computation"},{"key":"52_CR4","doi-asserted-by":"crossref","unstructured":"G. Gottlob, R. Pichler: Working with ARMs: Complexity Results on Atomic Representations of Herbrand Models, in Proceedings of LICS\u201999, pp. 306\u2013315, IEEE Computer Society Press, (1999).","DOI":"10.1109\/LICS.1999.782625"},{"key":"52_CR5","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"C. Kirchner, H. Kirchner, M. Rusinowitch: Deduction with symbolic constraints, Revue Fran\u00e7aise d\u2019Intelligence Artificielle, Vol 4, pp. 9\u201352 (1990).","journal-title":"Revue Fran\u00e7aise d\u2019Intelligence Artificielle"},{"key":"52_CR6","doi-asserted-by":"crossref","unstructured":"G. Kuper, K. McAloon, K. Palem, K. Perry: Efficient Parallel Algorithms for Anti-Unification and Relative Complement, in Proceedings of LICS\u201988, pp. 112\u2013120, IEEE Computer Society Press (1988).","DOI":"10.1109\/LICS.1988.5109"},{"key":"52_CR7","unstructured":"K. Kunen: Answer Sets and Negation as Failure, in Proceedings of the Fourth Int. Conf. on Logic Programming, Melbourne, pp. 219\u2013228 (1987)."},{"key":"52_CR8","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/BF00243794","volume":"3","author":"J.-L. Lassez","year":"1987","unstructured":"J.-L. Lassez, K. Marriott: Explicit Representation of Terms defined by Counter Examples, Journal of Automated Reasoning, Vol 3, pp. 301\u2013317 (1987).","journal-title":"Journal of Automated Reasoning"},{"key":"52_CR9","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Proceedings of MFCS\u201991","author":"J.-L. Lassez","year":"1991","unstructured":"J.-L. Lassez, M. Maher, K. Marriott: Elimination of Negation in Term Algebras, in Proceedings of MFCS\u201991, LNCS 520, pp. 1\u201316, Springer (1991)."},{"key":"52_CR10","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF01534454","volume":"15","author":"M. Maher","year":"1995","unstructured":"M. Maher, P. Stuckey: On Inductive Inference of Cyclic Structures, Annals of Mathematics and Artificial Intelligence Vol 15 No 2, pp. 167\u2013208, (1995).","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"52_CR11","volume-title":"PhD Thesis","author":"K. Marriott","year":"1988","unstructured":"K. Marriott: Finding Explicit Representations for Subsets of the Herbrand Universe, PhD Thesis, The University of Melbourne, Australia (1988)."},{"key":"52_CR12","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli, U. Montanari: An efficient unification algorithm, ACM Transactions on Programming Languages and Systems, Vol 4 No 2, pp. 258\u2013282 (1982).","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"52_CR13","unstructured":"R. Pichler: The Explicit Representability of Implicit Generalizations, to appear in Proceedings of RTA\u20192000, Springer (2000)."},{"key":"52_CR14","unstructured":"R. Pichler: Negation Elimination from Simple Equational Formulae, full paper, available from the author (2000)."},{"key":"52_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"L. J. Stockmeyer","year":"1976","unstructured":"L. J. Stockmeyer: The Polynomial Time Hierarchy, in Journal of Theoretical Computer Science, Vol 3, pp. 1\u201312 (1976).","journal-title":"Journal of Theoretical Computer Science"},{"key":"52_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-56868-9_24","volume-title":"Proceedings of RTA\u201993","author":"M. Tajine","year":"1993","unstructured":"M. Tajine: The negation elimination from syntactic equational formulas is decidable, in Proceedings of RTA\u201993, pp. 316\u2013327, LNCS 690, Springer (1993)."},{"key":"52_CR17","unstructured":"S. Vorobyov: An Improved Lower Bound for the Elementary Theories of Trees, in Proceedings of CADE-13, LNAI 1104, pp. 275\u2013287, Springer (1996)."}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45022-X_52","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,25]],"date-time":"2019-02-25T09:40:23Z","timestamp":1551087623000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45022-X_52"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677154","9783540450221"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-45022-x_52","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}