{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T12:40:14Z","timestamp":1737290414195,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664925"},{"type":"electronic","value":"9783540482420"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48242-3_18","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T16:28:09Z","timestamp":1184603289000},"page":"286-303","source":"Crossref","is-referenced-by-count":1,"title":["Simplification of Horn Clauses That Are Clausal Forms of Guarded Formulas"],"prefix":"10.1007","author":[{"given":"Michael","family":"Dierkes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"Hajnal Andr\u00e9ka, Johan van Benthem, and Istv\u00e1n Nemeti. Modal languages and bounded fragments of predicate logic. Research Report ML-96-03, ILLC, 1996."},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Ch. Bourely, R. Caferra, and N. Peltier. A method for building models automatically. Experiments with an extension of Otter. In Proceedings of CADE-12, pages 72\u201386. Springer, 1994. LNAI 814.","DOI":"10.1007\/3-540-58156-1_6"},{"key":"18_CR3","unstructured":"Michael Dierkes. Model building for guarded horn clauses. Research report, LEIBNIZ-IMAG Laboratory, 1999. Available via http:\/\/www-leibniz.imag.fr\/ATINF\/Michael.Dierkes\/articles\/mbghc.ps.gz ."},{"issue":"1","key":"18_CR4","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1093\/jigpal\/6.1.17","volume":"6","author":"C.G. Ferm\u00fcller","year":"1998","unstructured":"C.G. Ferm\u00fcller and A. Leitsch. Decision procedures and model building in equational clause logic. Journal of the IGPL, 6(1):17\u201341, 1998.","journal-title":"Journal of the IGPL"},{"issue":"2","key":"18_CR5","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"C. Ferm\u00fcller","year":"1996","unstructured":"Christian Ferm\u00fcller and A. Leitsch. Hyperresolution and automated model building. Journal of Logic and Computation, 6(2):173\u2013203, 1996.","journal-title":"Journal of Logic and Computation"},{"key":"18_CR6","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":"18_CR7","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":"18_CR8","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":"18_CR9","unstructured":"Nicolas Peltier. Nouvelles Techniques pour la Construction de Mod\u00e8les finis ou infinis en D\u00e9duction Automatique. PhD thesis, Institut National Polytechnique de Grenoble, 1997."},{"key":"18_CR10","volume-title":"Finder (finite domain enumerator): Notes and guides","author":"J. Slaney","year":"1992","unstructured":"J. Slaney. Finder (finite domain enumerator): Notes and guides. Technical report, Australian National University Automated Reasoning Project, Canberra, 1992."},{"key":"18_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/BFb0019355","volume-title":"Baltic Computer Science","author":"T. Tammet","year":"1991","unstructured":"Tanel Tammet. Using resolution for deciding solvable classes and building finite models. In Baltic Computer Science, pages 33\u201364. Springer, LNCS 502, 1991."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming and Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48242-3_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T12:00:16Z","timestamp":1737288016000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48242-3_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664925","9783540482420"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-48242-3_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}