{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T10:43:31Z","timestamp":1749725011604},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/bf00881950","type":"journal-article","created":{"date-parts":[[2004,12,25]],"date-time":"2004-12-25T19:25:12Z","timestamp":1104002712000},"page":"375-390","source":"Crossref","is-referenced-by-count":12,"title":["A tableau prover for domain minimization"],"prefix":"10.1007","volume":"13","author":[{"given":"Sven","family":"Lorenz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"Beckert, B. and H\ufffdhnle, R.: An improved method for adding equality to free variable semantic tableau, in D. Kapur (ed.),Proc. CADE-11, Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_188"},{"key":"CR2","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0004-3702(80)90013-2","volume":"13","author":"M. Davis","year":"1980","unstructured":"Davis, M.: The mathematics of non-monotonic reasoning,Artificial Intelligence 13 (1980), 73?80.","journal-title":"Artificial Intelligence"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/0004-3702(87)90081-6","volume":"31","author":"D. W. Etherington","year":"1987","unstructured":"Etherington, D. W.: Formalizing nonmonotonic reasoning systems,Artificial Intelligence 31 (1987), 41?85.","journal-title":"Artificial Intelligence"},{"key":"CR4","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1111\/j.1467-8640.1987.tb00177.x","volume":"3","author":"D. W. Etherington","year":"1987","unstructured":"Etherington, D. W. and Mercer, R. E.: Domain circumscription: A reevaluation,Computational Intelligence 3 (1987), 94?99.","journal-title":"Computational Intelligence"},{"key":"CR5","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1111\/j.1467-8640.1985.tb00055.x","volume":"1","author":"D. W. Etherington","year":"1985","unstructured":"Etherington, D. W., Mercer, R. E., and Reiter, R.: On the adequacy of predicate circumscription for closed-world reasoning,Computational Intelligence 1 (1985), 11?15.","journal-title":"Computational Intelligence"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Fitting, M.:First-Order Logic and Automated Theorem Proving, Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"CR7","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/0004-3702(89)90026-X","volume":"39","author":"M. L. Ginsberg","year":"1989","unstructured":"Ginsberg, M. L.: A circumscriptive theorem prover,Artificial Intelligence 39 (1989), 209?230.","journal-title":"Artificial Intelligence"},{"key":"CR8","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/BF00881956","volume":"13","author":"R. H\ufffdhnle","year":"1994","unstructured":"H\ufffdhnle, R. and Schmitt, P.: The liberalized ?-rule in free variable semantic tableaux,J. Automated Reasoning 13 (1994), 211.","journal-title":"J. Automated Reasoning"},{"key":"CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00244510","volume":"4","author":"J. Hintikka","year":"1988","unstructured":"Hintikka, J.: Model minimization ? and alternative to circumscription,J. Automated Reasoning 4 (1988), 1?13.","journal-title":"J. Automated Reasoning"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"Lorenz, S.: Nonmonotonic temporal reasoning: Persistence, justified causation, and event minimization, in Z. W. Ras and M. Zemankova (eds),Methodologies for Intelligent Systems VI, Springer-Verlag, 1991.","DOI":"10.1007\/3-540-54563-8_117"},{"key":"CR11","unstructured":"Lorenz, S.: Temporales Schlie\ufffden unter Standardannahmen bei der Verarbeitung nat\ufffdrlicher Sprache. PhD thesis, Universit\ufffdt Stuttgart, 1993."},{"key":"CR12","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/0004-3702(86)90032-9","volume":"13","author":"J. McCarthy","year":"1986","unstructured":"McCarthy, J.: Applications of circumscription to formalizing commonsense knowledge,Artificial Intelligence 13 (1986), 89?116.","journal-title":"Artificial Intelligence"},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"McCarthy, J.: Circumscription ? a form of non-monotonic reasoning,Artificial Intelligence 13 (1980).","DOI":"10.21236\/ADA086574"},{"key":"CR14","unstructured":"McCarthy, J.: Epistemological problems of artificial intelligence, inProc. IJCAI 77, 1977, pp. 1038?1044."},{"key":"CR15","unstructured":"Murray, N. V. and Rosenthal, E.: On the relative merits of path dissolution and the method of analytic tableaux. Technical Report 90-5, SUNY at Albany, Albany, 1991."},{"key":"CR16","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/BF00247828","volume":"9","author":"N. Olivetti","year":"1992","unstructured":"Olivetti, N.: Tableaux and sequent calculus for minimal entailment,J. Automated Reasoning 9 (1992), 99?139.","journal-title":"J. Automated Reasoning"},{"key":"CR17","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/BF00244513","volume":"4","author":"F. Oppacher","year":"1988","unstructured":"Oppacher, F. and Suen, E.: Harp: A tableau-based theorem prover,J. Automated Reasoning 4 (1988), 69?100.","journal-title":"J. Automated Reasoning"},{"key":"CR18","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0004-3702(89)90067-2","volume":"38","author":"T. C. Przymusinski","year":"1989","unstructured":"Przymusinski, T. C.: An algorithm to computer circumscription,Artificial Intelligence 38 (1989), 49?73.","journal-title":"Artificial Intelligence"},{"key":"CR19","series-title":"Technical Report 87.9.7","volume-title":"The thot theorem prover","author":"P. H. Schmitt","year":"1987","unstructured":"Schmitt, P. H.: The thot theorem prover. Technical Report 87.9.7, IBM Deutschland GmbH, Heidelberg, 1987."},{"key":"CR20","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/BF00881837","volume":"10","author":"M. Suchenek","year":"1993","unstructured":"Suchenek, M.: First-order syntactic characterizations of minimal entailment, domain-minimal entailment, and Herbrand entailment,J. Automated Reasoning 10 (1993), 237?263.","journal-title":"J. Automated Reasoning"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881950.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881950\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881950","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T23:29:59Z","timestamp":1586042999000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881950"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"references-count":20,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1994]]}},"alternative-id":["BF00881950"],"URL":"https:\/\/doi.org\/10.1007\/bf00881950","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}