{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:10:04Z","timestamp":1749125404155,"version":"3.41.0"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2002,3,1]],"date-time":"2002-03-01T00:00:00Z","timestamp":1014940800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,3,1]],"date-time":"2002-03-01T00:00:00Z","timestamp":1014940800000},"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":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2002,3]]},"DOI":"10.1023\/a:1020512924736","type":"journal-article","created":{"date-parts":[[2003,3,18]],"date-time":"2003-03-18T20:12:43Z","timestamp":1048018363000},"page":"17-57","source":"Crossref","is-referenced-by-count":4,"title":["Ordered Semantic Hyper Tableaux"],"prefix":"10.1007","volume":"29","author":[{"given":"Adnan","family":"Yahya","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David A.","family":"Plaisted","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5092908_CR1","doi-asserted-by":"crossref","unstructured":"Baumgartner, P.: FDPLL \u2014 a first-order Davis\u2014Putnam\u2014Logemann\u2014Loveland procedure, in Proceedings of CADE, LNAI 1831, Springer-Verlag, 2000, pp. 200\u2013219.","DOI":"10.1007\/10721959_16"},{"key":"5092908_CR2","doi-asserted-by":"crossref","unstructured":"Baumgartner, P.: Hyper tableaux \u2014 the next generation, in Proceedings of TABLEAUX'98, LNCS 1397, Springer-Verlag, 1998, pp. 60\u201376.","DOI":"10.1007\/3-540-69778-0_14"},{"key":"5092908_CR3","unstructured":"Baumgartner, P., Fr\u00f6hlich, P., Furbach, U. and Nejdl, W.: Semantically guided theorem proving for diagnosis applications, in Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 97), 1997, pp. 460\u2013465."},{"key":"5092908_CR4","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/BFb0027406","volume-title":"Proceedings of the Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'97)","author":"P. Baumgartner","year":"1997","unstructured":"Baumgartner, P., Fr\u00f6hlich, P., Furbach, U. and Nejdl, W.: Tableaux for diagnosis applications, in Proceedings of the Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'97), LNAI 1227, Springer-Verlag, New York, 1997, pp. 76\u201390."},{"issue":"5","key":"5092908_CR5","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1006\/jsco.1993.1058","volume":"16","author":"P. Baumgartner","year":"1993","unstructured":"Baumgartner, P. and Furbach, U.: Consolution as a framework for comparing calculi, J. Symbolic Comput.\n16(5) (1993), 445\u2013477.","journal-title":"J. Symbolic Comput."},{"key":"5092908_CR6","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Furbach, U. and Niemal\u00e4, I.: Hyper tableaux, in Proceedings of JELIA'96, LNAI 1126, Springer-Verlag, 1996, pp. 1\u201317.","DOI":"10.1007\/3-540-61630-6_1"},{"key":"5092908_CR7","doi-asserted-by":"crossref","unstructured":"Billon, J.-P.: The disconnection method \u2014 a confluent integration of unification in the analytic framework, in Proceedings of the Fifth Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Palermo, Italy, LNCS 1071 Springer-Verlag, May 1996, pp. 110\u2013126.","DOI":"10.1007\/3-540-61208-4_8"},{"key":"5092908_CR8","unstructured":"Brown, M. and Sutcliffe, G.: PTTP+GLiDeS: Using models to guide linear deductions, in Proceedings of CADE-17 Workshop: Model Computation \u2014 Principles, Algorithms, Applications, June 2000, pp. 42\u201345."},{"issue":"1","key":"5092908_CR9","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1023\/A:1006291616338","volume":"25","author":"F. Bry","year":"2000","unstructured":"Bry, F. and Yahya, A.: Positive unit hyperresolution tableaux and their application to minimal model generation, J. Automated Reasoning\n25(1) (2000), 35\u201382.","journal-title":"J. Automated Reasoning"},{"key":"5092908_CR10","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/BF00881886","volume":"12","author":"T. Chou","year":"1994","unstructured":"Chou, T. and Winslett, M.: A model-based belief revision system, J. Automated Reasoning\n12 (1994), 157\u2013208.","journal-title":"J. Automated Reasoning"},{"key":"5092908_CR11","doi-asserted-by":"crossref","unstructured":"Chu, H. and Plaisted, D.: Semantically guided first order theorem proving using hyperlinking, in Proceedings of CADE-12, LNAI 814, Springer-Verlag, 1994, pp. 192\u2013206.","DOI":"10.1007\/3-540-58156-1_14"},{"key":"5092908_CR12","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1016\/0304-3975(51)90010-2","volume":"78","author":"R. Demolombe","year":"1991","unstructured":"Demolombe, R.: An efficient strategy for non-Horn deductive databases, Theoret. Comput. Sci.\n78 (1991), 245\u2013259.","journal-title":"Theoret. Comput. Sci."},{"key":"5092908_CR13","unstructured":"Eder, E.: Consolution and its relation with resolution, in Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI-91), Morgan Kaufmann, August 1991, pp. 132\u2013136."},{"key":"5092908_CR14","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":"5092908_CR15","volume-title":"Using a modified size measure to guide the search in the ordered semantic hyperlinking theorem prover","author":"S. Funk","year":"2000","unstructured":"Funk, S.: Using a modified size measure to guide the search in the ordered semantic hyperlinking theorem prover, M.S. thesis, University of North Carolina at Chapel Hill, April 2000."},{"key":"5092908_CR16","doi-asserted-by":"crossref","unstructured":"Haehnle, R. and Pape, C.: Ordered tableaux: Extensions and applications, in Proceedings of Conference on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX'97), 1997, pp. 173\u2013187.","DOI":"10.1007\/BFb0027413"},{"key":"5092908_CR17","doi-asserted-by":"crossref","unstructured":"Hasegawa, R., Inoue, K., Ohta, Y. and Koshimura, M.: Nonhorn magic sets to incorporate topdown inference into bottom-up theorem proving, in Proceedings of CADE97, 1997, pp. 176\u2013190.","DOI":"10.1007\/3-540-63104-6_18"},{"key":"5092908_CR18","unstructured":"Johnson, C. A.: Top down deduction in indefinite deductive databases, in Journ\u00e9es Bases de Donn\u00e9es Avanc\u00e9es, Toulouse, France, 1993, pp. 119\u2013138."},{"key":"5092908_CR19","doi-asserted-by":"crossref","unstructured":"Letz, R.: Using matings for pruning connection tableaux, in Proceedings of CADE-15, LNAI 1421, Springer-Verlag, 1998, pp. 381\u2013396.","DOI":"10.1007\/BFb0054273"},{"key":"5092908_CR20","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"Letz, R., Mayr, K. and Goller, C.: Controlled integration of the cut rule into connection tableau calculi, J. Automated Reasoning\n13 (1994), 119\u2013138.","journal-title":"J. Automated Reasoning"},{"key":"5092908_CR21","doi-asserted-by":"crossref","unstructured":"Letz, R. and Stenz, G.: DCTP \u2014 a disconnection calculus theorem prover-system (Abstract), in Proceedings of IJCAR2001, June 2001, pp. 381\u2013385.","DOI":"10.1007\/3-540-45744-5_30"},{"key":"5092908_CR22","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/BF00881861","volume":"14","author":"D. W. Loveland","year":"1995","unstructured":"Loveland, D. W., Reed, D. and Wilson, D.: SATCHMORE: SATCHMO with relevancy, J. Automated Reasoning\n14 (1995), 349\u2013363.","journal-title":"J. Automated Reasoning"},{"key":"5092908_CR23","unstructured":"Loveland, D. W. and Yahya, A.: SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy, New Generation Computing, to appear."},{"key":"5092908_CR24","doi-asserted-by":"crossref","unstructured":"Manthey, R. and Bry, F.: Satchmo: A theorem prover implemented in Prolog, in Proceedings of CADE88, 1988, pp. 415\u2013434.","DOI":"10.1007\/BFb0012847"},{"key":"5092908_CR25","unstructured":"Nejdl, W. and Fr\u00f6hlich, P.: Minimal model semantics for diagnosis applications: Techniques and first benchmarks, in Proceedings of the 7th International Workshop on the Principles of Diagnostics, 1996."},{"key":"5092908_CR26","doi-asserted-by":"crossref","unstructured":"Niemel\u00e4, I.: A tableau calculus for minimal model reasoning, in P. Miglioli, U. Moscato, D. Mundici and M. Ornaghi (eds), Proceedings of the FifthWorkshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 1071, Springer-Verlag, 1996, pp. 278\u2013294.","DOI":"10.1007\/3-540-61208-4_18"},{"issue":"3","key":"5092908_CR27","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1023\/A:1006376231563","volume":"25","author":"D. Plaisted","year":"2000","unstructured":"Plaisted, D. and Zhu, Y.: Ordered semantic hyper-linking, J. Automated Reasoning\n25(3) (2000), 167\u2013217.","journal-title":"J. Automated Reasoning"},{"key":"5092908_CR28","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/BF00249019","volume":"7","author":"A. Ramsay","year":"1991","unstructured":"Ramsay, A.: Generating relevant models, J. Automated Reasoning\n7 (1991), 359\u2013368.","journal-title":"J. Automated Reasoning"},{"key":"5092908_CR29","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF01530824","volume":"14","author":"A. Rajasekar","year":"1995","unstructured":"Rajasekar, A. and Yusuf, H.: Dwam \u2014 a WAM model extension for disjunctive logic programming, Ann. Math. Artificial Intelligence\n14 (1995), 275\u2013308.","journal-title":"Ann. Math. Artificial Intelligence"},{"key":"5092908_CR30","doi-asserted-by":"crossref","unstructured":"Smullyan, R.: First Order Logic, Springer-Verlag, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"5092908_CR31","unstructured":"Yahya, A.: A goal-driven approach to efficient query processing in disjunctive deductive databases, Technical Report PMS-FB-1996-12, Department of Computer Science, Munich University, July 1996."},{"issue":"1","key":"5092908_CR32","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF00881914","volume":"13","author":"A. Yahya","year":"1994","unstructured":"Yahya, A., Fernandez, J. A. and Minker, J.: Ordered model trees: A normal form for disjunctive deductive databases, J. Automated Reasoning\n13(1) (1994), 117\u2013144.","journal-title":"J. Automated Reasoning"},{"key":"5092908_CR33","unstructured":"Zhu, Y. and Plaisted, D.: FOLPLAN: A semantically guided first-order planner, in 10th International FLAIRS Conference, Daytona Beach, Florida, May 11\u201314, 1997."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1020512924736.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1020512924736\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1020512924736.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:35:10Z","timestamp":1749123310000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1020512924736"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,3]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,3]]}},"alternative-id":["5092908"],"URL":"https:\/\/doi.org\/10.1023\/a:1020512924736","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2002,3]]}}}