{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:18:25Z","timestamp":1725535105657},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Many Automated Theorem Proving (ATP) systems for different logics,<\/jats:p><jats:p>and translators for translating different logics from one to another,<\/jats:p><jats:p>have been developed and are now available.<\/jats:p><jats:p>Some logics are more expressive than others, and it is easier to express problems in those logics.<\/jats:p><jats:p>However, their ATP systems are relatively newer,<\/jats:p><jats:p>and need more development and testing in order to solve more problems in a reasonable time.<\/jats:p><jats:p>To benefit from the available tools to solve more problems in more expressive logics,<\/jats:p><jats:p>different ATP systems and translators can be combined.<\/jats:p><jats:p>Problems in logics more expressive than CNF can be translated directly to CNF, or indirectly by translation via intermediate logics.<\/jats:p><jats:p>Description Logic (DL) sits between CNF and propositional logic.<\/jats:p><jats:p>Saffron a CNF to DL translator, has been developed, which fills the gap between CNF and DL.<\/jats:p><jats:p>ATP by translation to DL is now an alternative way of solving problems expressed in logics more expressive than DL,<\/jats:p><jats:p>by combining necessary translators from those logics to CNF, Saffron, and a DL ATP system.<\/jats:p>","DOI":"10.29007\/xgq9","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:04:15Z","timestamp":1516730655000},"page":"1--14","source":"Crossref","is-referenced-by-count":0,"title":["Automated Theorem Proving by Translation to Description Logic"],"prefix":"10.29007","volume":"35","author":[{"given":"Negin","family":"Arhami","sequence":"first","affiliation":[]},{"given":"Geoff","family":"Sutcliffe","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"LPAR-20. 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:05:15Z","timestamp":1516730715000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/XVw"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/xgq9","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}