{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:31:18Z","timestamp":1742913078327,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642224379"},{"type":"electronic","value":"9783642224386"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22438-6_24","type":"book-chapter","created":{"date-parts":[[2011,7,18]],"date-time":"2011-07-18T18:21:44Z","timestamp":1311013304000},"page":"315-330","source":"Crossref","is-referenced-by-count":0,"title":["Predicate Completion for non-Horn Clause Sets"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Horbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"24_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. of Logic and Computation\u00a04(3), 217\u2013247 (1994)","journal-title":"J. of Logic and Computation"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/3-540-15976-2_11","volume-title":"Rewriting Techniques and Applications","author":"L. Bachmair","year":"1985","unstructured":"Bachmair, L., Plaisted, D.A.: Associative path orderings. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol.\u00a0202, pp. 241\u2013254. Springer, Heidelberg (1985)"},{"key":"24_CR3","first-page":"293","volume-title":"Logic and Data Bases","author":"K.L. Clark","year":"1977","unstructured":"Clark, K.L.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, pp. 293\u2013322. Plenum Press, New York (1977)"},{"issue":"2","key":"24_CR4","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1994.1056","volume":"112","author":"H. Comon","year":"1994","unstructured":"Comon, H., Delor, C.: Equational formulae with membership constraints. Information and Computation\u00a0112(2), 167\u2013216 (1994)","journal-title":"Information and Computation"},{"issue":"3-4","key":"24_CR5","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H. Comon","year":"1989","unstructured":"Comon, H., Lescanne, P.: Equational problems and disunification. Journal of Symbolic Computation\u00a07(3-4), 371\u2013425 (1989)","journal-title":"Journal of Symbolic Computation"},{"issue":"1\/2","key":"24_CR6","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1006\/inco.2000.2875","volume":"159","author":"H. Comon","year":"2000","unstructured":"Comon, H., Nieuwenhuis, R.: Induction = I-Axiomatization + First-Order Consistency. Information and Computation\u00a0159(1\/2), 151\u2013186 (2000)","journal-title":"Information and Computation"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/3-540-56393-8_17","volume-title":"Conditional Term Rewriting Systems","author":"H. Ganzinger","year":"1993","unstructured":"Ganzinger, H., Stuber, J.: Inductive theorem proving by consistency for first-order clauses. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol.\u00a0656, pp. 226\u2013241. Springer, Heidelberg (1993)"},{"issue":"2\/3&4","key":"24_CR8","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1016\/0743-1066(93)90035-F","volume":"17","author":"M. Gelfond","year":"1993","unstructured":"Gelfond, M., Lifschitz, V.: Representing action and change by logic programs. Journal of Logic Programming\u00a017(2\/3&4), 301\u2013321 (1993)","journal-title":"Journal of Logic Programming"},{"key":"24_CR9","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-17511-4_17","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Horbach","year":"2010","unstructured":"Horbach, M.: Disunification for ultimately periodic interpretations. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS (LNAI), vol.\u00a06355, pp. 290\u2013311. Springer, Heidelberg (2010)"},{"key":"24_CR10","series-title":"LNAI","first-page":"315","volume-title":"CADE-23","author":"M. Horbach","year":"2011","unstructured":"Horbach, M.: System description: SPASS-FD. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol.\u00a06803, pp. 315\u2013321. Springer, Heidelberg (2011)"},{"key":"24_CR11","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-642-02959-2_30","volume-title":"Automated Deduction \u2013 CADE-22","author":"M. Horbach","year":"2009","unstructured":"Horbach, M., Weidenbach, C.: Decidability results for saturation-based model building. In: Schmidt, R. (ed.) CADE-22. LNCS (LNAI), vol.\u00a05663, pp. 404\u2013420. Springer, Heidelberg (2009)"},{"issue":"4","key":"24_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1805950.1805957","volume":"11","author":"M. Horbach","year":"2010","unstructured":"Horbach, M., Weidenbach, C.: Superposition for fixed domains. ACM Transactions on Computational Logic\u00a011(4), 27:1\u201327:35 (2010)","journal-title":"ACM Transactions on Computational Logic"},{"key":"24_CR13","first-page":"73","volume-title":"TIME 2009","author":"M. Ludwig","year":"2009","unstructured":"Ludwig, M., Hustadt, U.: Resolution-based model construction for PLTL. In: Lutz, C., Raskin, J.-F. (eds.) TIME 2009, pp. 73\u201380. IEEE Computer Society, Los Alamitos (2009)"},{"key":"24_CR14","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/0004-3702(86)90032-9","volume":"28","author":"J. McCarthy","year":"1986","unstructured":"McCarthy, J.: Applications of circumscription to formalizing common sense knowledge. Artificial Intelligence\u00a028, 89\u2013116 (1986)","journal-title":"Artificial Intelligence"},{"issue":"1-2","key":"24_CR15","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/S0004-3702(97)00007-6","volume":"92","author":"X. Nie","year":"1997","unstructured":"Nie, X.: Non-horn clause logic programming. Artificial Intelligence\u00a092(1-2), 243\u2013258 (1997)","journal-title":"Artificial Intelligence"},{"issue":"1-2","key":"24_CR16","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/0004-3702(80)90014-4","volume":"13","author":"R. Reiter","year":"1980","unstructured":"Reiter, R.: A logic for default reasoning. Artificial Intelligence\u00a013(1-2), 81\u2013132 (1980)","journal-title":"Artificial Intelligence"},{"key":"24_CR17","first-page":"418","volume-title":"AAAI","author":"R. Reiter","year":"1982","unstructured":"Reiter, R.: Circumscription implies predicate completion (sometimes). In: Waltz, D.L. (ed.) AAAI, pp. 418\u2013420. AAAI Press, Menlo Park (1982)"},{"key":"24_CR18","first-page":"328","volume-title":"LICS","author":"P.J. Stuckey","year":"1991","unstructured":"Stuckey, P.J.: Constructive negation for constraint logic programming. In: LICS, pp. 328\u2013339. IEEE Computer Society, Los Alamitos (1991)"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/BFb0018387","volume-title":"Knowledge Based Computer Systems","author":"A. Togashi","year":"1990","unstructured":"Togashi, A., Hou, B.-H., Noguchi, S.: Generalized predicate completion. In: Ramani, S., Anjaneyulu, K., Chandrasekar, R. (eds.) KBCS 1989. LNCS, vol.\u00a0444, pp. 286\u2013295. Springer, Heidelberg (1990)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-23"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22438-6_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,30]],"date-time":"2019-03-30T02:57:44Z","timestamp":1553914664000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22438-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642224379","9783642224386"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22438-6_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}