{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T21:40:12Z","timestamp":1737063612641,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677970"},{"type":"electronic","value":"9783540449577"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44957-4_39","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T05:24:41Z","timestamp":1180675481000},"page":"583-597","source":"Crossref","is-referenced-by-count":0,"title":["An Application of Model Building in a Resolution Decision Procedure for Guarded Formulas"],"prefix":"10.1007","author":[{"given":"Michael","family":"Dierkes","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,12,15]]},"reference":[{"issue":"3","key":"39_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1023\/A:1004275029985","volume":"27","author":"H. Andr\u00e9ka","year":"1998","unstructured":"Hajnal Andr\u00e9ka, Johan van Benthem, and Istv\u00e1n Nemeti. Modal logics and bounded fragments of predicate logic. Journal of Philosophical Logic, 27(3):217\u2013274, 1998.","journal-title":"Journal of Philosophical Logic"},{"key":"39_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of CADE-10","author":"L. Bachmair","year":"1990","unstructured":"L. Bachmair and H. Ganzinger. On restrictions of ordered paramodulation with simplification. In Proceedings of CADE-10, volume 449 of LNCS. Springer, 1990."},{"key":"39_CR3","unstructured":"Homepage of the Bliksem theorem prover. http:\/\/www.mpi-sb.mpg.de\/~bliksem\/ ."},{"key":"39_CR4","unstructured":"R. Caferra and N. Peltier. Extending semantic resolution via automated model building: applications. In Proceeding of IJCAI\u201995, pages 328\u2013334. Morgan Kaufman, 1995."},{"key":"39_CR5","unstructured":"M. Dierkes. Defining a unique Herbrand model for sets of guarded clauses. Accepted for International Workshop on First Order Theorem Proving FTP\u20192000."},{"key":"39_CR6","doi-asserted-by":"crossref","unstructured":"M. Dierkes. Simplification of Horn clauses that are clausal forms of guarded formulas. In Proceedings of LPAR\u201999, volume 1705 of LNAI. Springer, 1999.","DOI":"10.1007\/3-540-48242-3_18"},{"key":"39_CR7","doi-asserted-by":"crossref","unstructured":"H. Ganzinger, Ch. Meyer, and Ch Weidenbach. Soft typing for ordered resolution. In Proceedings of CADE-14, volume 1249 of LNAI. Springer, 1997.","DOI":"10.1007\/3-540-63104-6_32"},{"key":"39_CR8","doi-asserted-by":"crossref","unstructured":"H. Ganzinger and H. de Nivelle. A superposition decision procedure for the guarded fragment with equality. In Proc. 14th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1999.","DOI":"10.1109\/LICS.1999.782624"},{"key":"39_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"Proc. of CADE-9","author":"R. Manthey","year":"1988","unstructured":"Rainer Manthey and Fran\u00e7ois Bry. SATCHMO: A theorem prover implemented in Prolog. In Proc. of CADE-9, pages 415\u2013434. Springer, LNCS 310, 1988."},{"key":"39_CR10","doi-asserted-by":"crossref","unstructured":"Hans de Nivelle. Resolution decides the guarded fragment. Research Report CT-1998-01, ILLC, 1998.","DOI":"10.1007\/BFb0054260"},{"key":"39_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054260","volume-title":"Automated Deduction-CADE-15","author":"H. Nivelle de","year":"1998","unstructured":"Hans de Nivelle. A resolution decision procedure for the guarded fragment. In Automated Deduction-CADE-15, volume 1421 of LNCS, 1998."},{"key":"39_CR12","doi-asserted-by":"crossref","unstructured":"James R. Slagle. Automatic theorem proving with renamable and semantic resolution. Journal of the ACM, 14(4):687\u2013697, October 1967.","DOI":"10.1145\/321420.321428"},{"key":"39_CR13","first-page":"109","volume":"1","author":"J. Slaney","year":"1993","unstructured":"J. Slaney. Scott: a model-guided theorem prover. In Proceedings IJCAI-93, volume 1, pages 109\u2013114. Morgan Kaufmann, 1993.","journal-title":"Proceedings IJCAI-93"}],"container-title":["Lecture Notes in Computer Science","Computational Logic \u2014 CL 2000"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44957-4_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T21:04:09Z","timestamp":1737061449000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44957-4_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677970","9783540449577"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-44957-4_39","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}