{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:20Z","timestamp":1749124040144,"version":"3.40.5"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Mathematics and Artificial Intelligence"],"published-print":{"date-parts":[[2003,5]]},"DOI":"10.1023\/a:1022976016809","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T22:16:51Z","timestamp":1049753811000},"page":"211-228","source":"Crossref","is-referenced-by-count":5,"title":["Automated Deduction Techniques for the Management of Personalized Documents"],"prefix":"10.1007","volume":"38","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ulrich","family":"Furbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5118027_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1007\/3-540-69778-0_14","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"P. Baumgartner","year":"1998","unstructured":"P. Baumgartner, Hyper tableaux \u2013 the next generation, in: Automated Reasoning with Analytic Tableaux and Related Methods, ed. H. de Swaart, Lecture Notes in Artificial Intelligence, Vol. 1397 (Springer, Berlin, 1998) pp. 60\u201376."},{"key":"5118027_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/10721959_16","volume-title":"CADE-17 \u2013 The 17th International Conference on Automated Deduction","author":"P. Baumgartner","year":"2000","unstructured":"P. Baumgartner, FDPLL \u2013 a first-order Davis\u2013Putnam\u2013Logeman\u2013Loveland procedure, in: CADE-17 \u2013 The 17th International Conference on Automated Deduction, ed. D. McAllester, Lecture Notes in Artificial Intelligence, Vol. 1831 (Springer, Berlin, 2000) pp. 200\u2013219."},{"key":"5118027_CR3","volume-title":"Proc. JELIA 96","author":"P. Baumgartner","year":"1996","unstructured":"P. Baumgartner, U. Furbach and I. Niemel\u00e4, Hyper tableaux, in: Proc. JELIA 96 (Springer, Berlin, 1996)."},{"key":"5118027_CR4","series-title":"Lecture Notes in Artificial Intelligence","first-page":"1","volume-title":"KI-96: Advances in Artificial Intelligence","author":"S.-E. Bornscheuer","year":"1996","unstructured":"S.-E. Bornscheuer, Rational models of normal logic programs, in: KI-96: Advances in Artificial Intelligence, ed. S.H. G\u00fcnther G\u00f6rz, Lecture Notes in Artificial Intelligence, Vol. 1137 (Springer, Berlin, 1996) pp. 1\u20134."},{"key":"5118027_CR5","volume-title":"Programming in PROLOG","author":"W.F. Clocksin","year":"1981","unstructured":"W.F. Clocksin and C.S. Melish, Programming in PROLOG (Springer, Berlin, 1981)."},{"key":"5118027_CR6","volume-title":"Analysis Individuell","author":"I. Dahn","year":"2000","unstructured":"I. Dahn and H. Wolter, Analysis Individuell (Springer, Berlin, 2000)."},{"doi-asserted-by":"crossref","unstructured":"J. Dix, U. Furbach and I. Niemel\u00e4, Nonmonotonic reasoning: towards efficient calculi and implementations, in: Handbook of Automated Reasoning, eds. A. Voronkov and A. Robinson (Elsevier Science, 2001) pp. 1121\u20131234.","key":"5118027_CR7","DOI":"10.1016\/B978-044450813-3\/50021-7"},{"doi-asserted-by":"crossref","unstructured":"J. Dix and F. Stolzenburg, A framework to incorporate non-monotonic reasoning into constraint logic programming, Journal of Logic Programming 37(1\u20133), Special Issue on Constraint Logic Programming, eds. K. Marriott and P.J. Stuckey (1998) 47\u201376.","key":"5118027_CR8","DOI":"10.1016\/S0743-1066(98)10003-1"},{"key":"5118027_CR9","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/3-540-63255-7_14","volume-title":"Proceedings of the 4th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR-97)","author":"T. Eiter","year":"1997","unstructured":"T. Eiter, J. Lu and V.S. Subrahmanian, Computing non-ground representations of stable models, in: Proceedings of the 4th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR-97), eds. J. Dix, U. Furbach and A. Nerode (Springer, Berlin, 1997) pp. 198\u2013217."},{"issue":"2","key":"5118027_CR10","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"C. Ferm\u00fcller","year":"1996","unstructured":"C. Ferm\u00fcller and A. Leitsch, Hyperresolution and automated model building, Journal of Logic and Computation 6(2) (1996) 173\u2013230.","journal-title":"Journal of Logic and Computation"},{"unstructured":"M. Gelfond and V. Lifschitz, The stable model semantics for logic programming, in: Proceedings of the 5th International Conference on Logic Programming, Seattle, eds. R. Kowalski and K. Bowen (1988) pp. 1070\u20131080.","key":"5118027_CR11"},{"key":"5118027_CR12","doi-asserted-by":"crossref","first-page":"778","DOI":"10.1007\/3-540-58156-1_59","volume-title":"Automated Deduction \u2013 CADE 12, Nancy, France","author":"C. Goller","year":"1994","unstructured":"C. Goller, R. Letz, K. Mayr and J. Schumann, SETHEO V3.2: Recent developments \u2013 system abstract, in: Automated Deduction \u2013 CADE 12, Nancy, France, ed. A. Bundy (Springer, Berlin, 1994) pp. 778\u2013782."},{"issue":"1\u20132","key":"5118027_CR13","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/0304-3975(95)00207-3","volume":"166","author":"G. Gottlob","year":"1996","unstructured":"G. Gottlob, S. Marcus, A. Nerode, G. Salzer and V.S. Subrahmanian, A non-ground realization of the stable and well-founded semantics, Theoretical Computer Science 166(1\u20132) (1996) 221\u2013262.","journal-title":"Theoretical Computer Science"},{"key":"5118027_CR14","series-title":"Technical Report","volume-title":"ACID user manual \u2013 Version 1.0","author":"P. Graf","year":"1994","unstructured":"P. Graf, ACID user manual \u2013 Version 1.0, Technical Report MPI-I-94-DRAFT, Max-Planck-Institut, Saarbr\u00fccken, Germany (1994)."},{"issue":"3","key":"5118027_CR15","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1093\/jigpal\/8.3.239","volume":"8","author":"I. Horrocks","year":"2000","unstructured":"I. Horrocks, U. Sattler and S. Tobies, Practical reasoning for very expressive description logics, Logic Journal of the IGPL 8(3) (2000) 239\u2013263.","journal-title":"Logic Journal of the IGPL"},{"unstructured":"R. Letz, Clausal tableaux, in: Automated Deduction. A Basis for Applications, eds. W. Bibel and P.H. Schmitt (Kluwer Academic, 1998).","key":"5118027_CR16"},{"key":"5118027_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"Proceedings of the 9th Conference on Automated Deduction, Argonne, Illinois, May 1988","author":"R. Manthey","year":"1988","unstructured":"R. Manthey and F. Bry, SATCHMO: a theorem prover implemented in Prolog, in: Proceedings of the 9th Conference on Automated Deduction, Argonne, Illinois, May 1988, eds. E. Lusk and R. Overbeek, Lecture Notes in Computer Science, Vol. 310 (Springer, Berlin, 1988) pp. 415\u2013434."},{"key":"5118027_CR18","volume-title":"Proceedings of the Joint International Conference and Symposium on Logic Programming, Bonn, Germany","author":"I. Niemel\u00e4","year":"1996","unstructured":"I. Niemel\u00e4 and P. Simons, Efficient implementation of the well-founded and stable model semantics, in: Proceedings of the Joint International Conference and Symposium on Logic Programming, Bonn, Germany (The MIT Press, Cambridge, MA, 1996)."},{"issue":"2","key":"5118027_CR19","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/jigpal\/7.2.217","volume":"7","author":"N. Peltier","year":"1999","unstructured":"N. Peltier, Pruning the search space and extracting more models in tableaux, Logic Journal of the IGPL 7(2) (1999) 217\u2013251.","journal-title":"Logic Journal of the IGPL"},{"key":"5118027_CR20","first-page":"227","volume":"1","author":"J.A. Robinson","year":"1965","unstructured":"J.A. Robinson, Automated deduction with hyper-resolution, International Journal of Computational Mathematics 1 (1965) 227\u2013234.","journal-title":"International Journal of Computational Mathematics"},{"unstructured":"K. Sagonas, T. Swift and D.S. Warren, An abstract machine for computing the well-founded semantics, Journal of Logic Programming (2000), to appear.","key":"5118027_CR21"},{"key":"5118027_CR22","first-page":"337","volume-title":"Proceedings First International Conference on Deductive and Object-Oriented Databases (DOOD-89)","author":"C. Sakama","year":"1990","unstructured":"C. Sakama, Possible model semantics for disjunctive databases, in: Proceedings First International Conference on Deductive and Object-Oriented Databases (DOOD-89), eds. W. Kim, J.-M. Nicholas and S. Nishio (Elsevier Science\/North-Holland, Amsterdam, 1990) pp. 337\u2013351."},{"issue":"1","key":"5118027_CR23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(91)90078-X","volume":"48","author":"M. Schmidt-Schau\u00df","year":"1991","unstructured":"M. Schmidt-Schau\u00df and G. Smolka, Attributive concept descriptions with complements, Artificial Intelligence 48(1) (1991), 1\u201326.","journal-title":"Artificial Intelligence"},{"unstructured":"F. Stolzenburg, Loop-detection in hyper-tableaux by powerful model generation, Journal of Universal Computer Science 5(3), Special Issue on Integration of Deduction Systems, eds. R. H\u00e4hnle, W. Menzel, P.H. Schmitt and W. Reif (1999) 135\u2013155.","key":"5118027_CR24"},{"key":"5118027_CR25","doi-asserted-by":"crossref","first-page":"620","DOI":"10.1145\/116825.116838","volume":"38","author":"A. Van Gelder","year":"1991","unstructured":"A. Van Gelder, K.A. Ross and J.S. Schlipf, The well-founded semantics for general logic programs, Journal of the ACM 38 (1991) 620\u2013650.","journal-title":"Journal of the ACM"},{"key":"5118027_CR26","series-title":"Lecture Notes in Artificial Intelligence","first-page":"378","volume-title":"CADE-16 \u2013 The 16th International Conference on Automated Deduction, Trento, Italy","author":"C. Weidenbach","year":"1999","unstructured":"C. Weidenbach, B. Afshordel, U. Brahm, C. Cohrs, T. Engel, E. Keen, C. Theobalt and D. Topi\u0107, System description: SPASS Version 1.0.0, in: CADE-16 \u2013 The 16th International Conference on Automated Deduction, Trento, Italy, ed. H. Ganzinger, Lecture Notes in Artificial Intelligence, Vol. 1632 (Springer, Berlin, 1999) pp. 378\u2013382."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022976016809.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1022976016809\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022976016809.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:35:23Z","timestamp":1747546523000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1022976016809"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":26,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["5118027"],"URL":"https:\/\/doi.org\/10.1023\/a:1022976016809","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2003,5]]}}}