{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T03:28:17Z","timestamp":1725420497714},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>BDI (Bounded Depth Increase) is a new decidable<\/jats:p><jats:p>first-order clause class. It strictly includes<\/jats:p><jats:p>known classes such as PVD. The arity<\/jats:p><jats:p>of function and predicate symbols as well as the<\/jats:p><jats:p>shape of atoms is not restricted in BDI. Instead<\/jats:p><jats:p>the shape of \"cycles\" in resolution inferences is<\/jats:p><jats:p>restricted such that the depth of generated clauses<\/jats:p><jats:p>may increase but is still finitely bound.<\/jats:p><jats:p>The BDI class is motivated by real world problems<\/jats:p><jats:p>where function terms are used to represent record structures.<\/jats:p><jats:p>We show that the hyper-resolution calculus modulo<\/jats:p><jats:p>redundancy elimination terminates on BDI clause sets.<\/jats:p><jats:p>Employing this result to the ordered resolution calculus,<\/jats:p><jats:p>we can also prove termination of ordered resolution on BDI,<\/jats:p><jats:p>yielding a more efficient decision procedure.<\/jats:p>","DOI":"10.29007\/8m7f","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:02:53Z","timestamp":1516730573000},"page":"62-48","source":"Crossref","is-referenced-by-count":0,"title":["BDI: A New Decidable First-order Clause Class"],"prefix":"10.29007","volume":"26","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":"11545","event":{"name":"LPAR-19. 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:04:55Z","timestamp":1516730695000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/Ccc"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/8m7f","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}