{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T06:03:05Z","timestamp":1648792985932},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2005,11,1]],"date-time":"2005-11-01T00:00:00Z","timestamp":1130803200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Comput Sci Technol"],"published-print":{"date-parts":[[2005,11]]},"DOI":"10.1007\/s11390-005-0758-x","type":"journal-article","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T09:41:29Z","timestamp":1138182089000},"page":"758-762","source":"Crossref","is-referenced-by-count":1,"title":["Complexities of Homomorphism and Isomorphism for Definite Logic Programs"],"prefix":"10.1007","volume":"20","author":[{"given":"Dao-Yun","family":"Xu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhi-Hong","family":"Tao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"758_CR1","doi-asserted-by":"crossref","unstructured":"Cook S A, Reckhow R A. The relative efficiency of propositional proof system. Journal of Symbolic Logic, 1979, 44(1): 36\u201350, 2001.","DOI":"10.2307\/2273702"},{"key":"758_CR2","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/BF00265682","volume":"22","author":"B. Krishnamurthy","year":"1985","unstructured":"Krishnamurthy B. Short proofs for tricky formulas. Acta Informatica, 1985, 22: 253\u2013275.","journal-title":"Acta Informatica"},{"key":"758_CR3","unstructured":"Szeider S. How to Prove Unsatisfiability by Homomorphisms. Elsevier Preprint."},{"key":"758_CR4","doi-asserted-by":"crossref","unstructured":"Szeider S. NP-completeness of refutability by literal-once resolution. Lecture Notes in Artificial Intelligence 2083, Springer Verlag, Draft version, 2001.","DOI":"10.1007\/3-540-45744-5_13"},{"key":"758_CR5","doi-asserted-by":"crossref","unstructured":"Urquhart A. The complexity of propositional proofs. The Bulletin of Symbolic Logic, 1995, 1(4): 425\u2013467.","DOI":"10.2178\/bsl\/1203350879"},{"key":"758_CR6","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0166-218X(99)00039-6","volume":"96\u201397","author":"A. Urquhart","year":"1999","unstructured":"Urquhart A. The symmetry rule in propositional logic. Discrete Applied Mathematics, 1999, 96\u201397: 177\u2013193.","journal-title":"Discrete Applied Mathematics"},{"key":"758_CR7","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis M, Putnam H. A computing procedure for quantification theory. Journal of the ACM, 1960, 7: 201\u2013215.","journal-title":"Journal of the ACM"},{"key":"758_CR8","unstructured":"Daoyun Xu. On the complexity of renamings and homomorphisms for minimal unsatisfiable formulas [Dissertation]. Nanjing University, 2002."},{"issue":"2","key":"758_CR9","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1016\/S0166-218X(02)00411-0","volume":"130","author":"S. Szeider","year":"2003","unstructured":"Szeider S. Homomorphisms of conjunctive normal forms. Discrete Applied Mathematics, 2003, 130(2): 351\u2013356.","journal-title":"Discrete Applied Mathematics"},{"issue":"1","key":"758_CR10","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/0022-0000(88)90042-6","volume":"37","author":"C H Papadimitriou","year":"1988","unstructured":"Papadimitriou C H, Wolfe D. The complexity of facets resolved. Journal of Computer and System Sciences, 1988, 37(1): 2\u201313.","journal-title":"Journal of Computer and System Sciences"},{"key":"758_CR11","doi-asserted-by":"crossref","unstructured":"Aharoni R. Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas. Journal of Combinatorial Theory, Series A, 1996, 43(A): 196\u2013204.","DOI":"10.1016\/0097-3165(86)90060-9"},{"issue":"3-4","key":"758_CR12","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1023\/A:1018924526592","volume":"23","author":"G Davydov","year":"1998","unstructured":"G Davydov, I Davydova, H Kleine B\u00fcning. An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF. Annals of Mathematics and Artificial Intelligence, 1998, 23(3-4): 229\u2013245.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"1","key":"758_CR13","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/S0304-3975(01)00337-1","volume":"289","author":"H Fleischner","year":"2002","unstructured":"Fleischner H, Kullmann O, Szeider S. Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference. Theoretical Computer Science, 2002, 289(1): 503\u2013516.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"758_CR14","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/S0020-0190(02)00267-3","volume":"84","author":"H Kleine","year":"2002","unstructured":"H Kleine B\u00fcning, Xishun Zhao. Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency. Information Processing Letters, 2002, 84(3): 147\u2013151.","journal-title":"Information Processing Letters"},{"issue":"1\u20134","key":"758_CR15","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/s10472-004-9422-3","volume":"43","author":"H Kleine","year":"2005","unstructured":"H Kleine B\u00fcning, Daoyun Xu. The complexity of homomorphisms and renamings for minimal unsatisfiable formulas. Annals of Mathematics and Artificial Intelligence, 2005, 43(1\u20134): 113\u2013127.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"758_CR16","doi-asserted-by":"crossref","unstructured":"K\u00f6bler J, Sch\u00f6ning J, Toran J. The Graph Isomorphism Problem: Its Structural Complexity. Birkh\u00e4user Verlag, 1993.","DOI":"10.1007\/978-1-4612-0333-9"},{"key":"758_CR17","doi-asserted-by":"crossref","unstructured":"Hell P, Ne\u0161et\u0159il J. On the complexity of H-coloring. Journal of Combinatorial Theory, Series B, 1990, 48: 92\u2013110.","DOI":"10.1016\/0095-8956(90)90132-J"},{"key":"758_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-349-03521-2","volume-title":"Graph Theory with Applications","author":"J A Bondy","year":"1976","unstructured":"Bondy J A, Murty U S R. Graph Theory with Applications. London: Macmillan, 1976."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-005-0758-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-005-0758-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-005-0758-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,12]],"date-time":"2020-04-12T08:34:08Z","timestamp":1586680448000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-005-0758-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,11]]},"references-count":18,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2005,11]]}},"alternative-id":["758"],"URL":"https:\/\/doi.org\/10.1007\/s11390-005-0758-x","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,11]]}}}