{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:03Z","timestamp":1747592463635},"reference-count":16,"publisher":"Oxford University Press (OUP)","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,3]]},"DOI":"10.1093\/logcom\/exu074","type":"journal-article","created":{"date-parts":[[2014,12,9]],"date-time":"2014-12-09T20:46:19Z","timestamp":1418157979000},"page":"441-468","source":"Crossref","is-referenced-by-count":5,"title":["BDI: a new decidable clause class"],"prefix":"10.1093","volume":"27","author":[{"given":"Manuel","family":"Lamotte-Schubert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2014,12,8]]},"reference":[{"key":"key\n\t\t\t\t20170315215008_B1","first-page":"4:1","article-title":"New results on rewrite-based satisfiability procedures","volume-title":"ACM Transactions on Computational Logic","year":"2009"},{"key":"key\n\t\t\t\t20170315215008_B2","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","article-title":"Resolution theorem provin?","volume-title":"Handbook of Automated Reasoning","year":"2001"},{"key":"key\n\t\t\t\t20170315215008_B3","first-page":"83","article-title":"Superposition with simplification as a decision procedure for the monadic class with equalit?","volume-title":"Computational Logic and Proof Theory, Third Kurt G\u00f6del Colloquium","year":"1993"},{"key":"key\n\t\t\t\t20170315215008_B4","volume-title":"The Classical Decision Problem","year":"1996"},{"key":"key\n\t\t\t\t20170315215008_B5","volume-title":"Resolution Methods for the Decision Problem","year":"1993"},{"key":"key\n\t\t\t\t20170315215008_B6","doi-asserted-by":"crossref","first-page":"1791","DOI":"10.1016\/B978-044450813-3\/50027-8","article-title":"Resolution decision procedure?","volume-title":"Handbook of Automated Reasoning","year":"2001"},{"key":"key\n\t\t\t\t20170315215008_B7","first-page":"2003","article-title":"Hyperresolution for guarded formulae","volume":"36","year":"2000","journal-title":"Journal of Symbolic Computation"},{"key":"key\n\t\t\t\t20170315215008_B8","first-page":"260","article-title":"A new clausal class decidable by hyperresolutio?","volume-title":"Automated DeductionCADE-18","year":"2002"},{"key":"key\n\t\t\t\t20170315215008_B9","first-page":"251","article-title":"A survey of decidable first-order fragments and description logics","volume":"1","year":"2004","journal-title":"Journal of Relational Methods in Computer Science"},{"key":"key\n\t\t\t\t20170315215008_B10","first-page":"557","article-title":"Tree automata with equality constraints modulo equational theories","volume-title":"Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings","year":"2006"},{"key":"key\n\t\t\t\t20170315215008_B11","first-page":"90","article-title":"Analysis of authorizations in SAP R\/3","volume-title":"FTP 2009: First-Order Theorem Proving","year":"2009"},{"key":"key\n\t\t\t\t20170315215008_B12","article-title":"A suggestion for an n-ary description logic","volume-title":"Proceedings of the 1999 International Workshop on Description Logics (DL'99), Link\u00f6ping, Sweden, July 30 - August 1, Vol. 22 of CEUR Workshop Proceedings","year":"1999"},{"key":"key\n\t\t\t\t20170315215008_B13","article-title":"Resolution decides the guarded fragment, 1998","volume-title":"ILLC Report CT-98-01"},{"key":"key\n\t\t\t\t20170315215008_B14","first-page":"255","article-title":"A variant of a recursively unsolvable problem","volume":"12","year":"1946","journal-title":"Journal of Symbolic Logic"},{"key":"key\n\t\t\t\t20170315215008_B15","first-page":"314","article-title":"Towards an automatic analysis of security protocols in first-order logi?","volume-title":"16th International Conference on Automated Deduction, CADE-16","year":"1999"},{"key":"key\n\t\t\t\t20170315215008_B16","doi-asserted-by":"crossref","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","article-title":"Combining superposition, sorts and splittin?","volume-title":"Handbook of Automated Reasoning","year":"2001"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/27\/2\/441\/10987552\/exu074.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,24]],"date-time":"2017-08-24T21:43:23Z","timestamp":1503611003000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/2687720\/BDI:"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,8]]},"references-count":16,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2014,12,8]]},"published-print":{"date-parts":[[2017,3]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exu074","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,12,8]]}}}