{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T07:59:52Z","timestamp":1730275192362,"version":"3.28.0"},"reference-count":26,"publisher":"IEEE","license":[{"start":{"date-parts":[[2019,11,1]],"date-time":"2019-11-01T00:00:00Z","timestamp":1572566400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2019,11,1]],"date-time":"2019-11-01T00:00:00Z","timestamp":1572566400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2019,11,1]],"date-time":"2019-11-01T00:00:00Z","timestamp":1572566400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,11]]},"DOI":"10.1109\/iske47853.2019.9170395","type":"proceedings-article","created":{"date-parts":[[2020,8,18]],"date-time":"2020-08-18T21:10:34Z","timestamp":1597785034000},"page":"69-73","source":"Crossref","is-referenced-by-count":1,"title":["A First-Order Logic Clause Set Preprocessing Method Based on Clause Deduction Distance"],"prefix":"10.1109","author":[{"given":"Feng","family":"Cao","sequence":"first","affiliation":[]},{"given":"Yang","family":"Xu","sequence":"additional","affiliation":[]},{"given":"ShuWei","family":"Chen","sequence":"additional","affiliation":[]},{"given":"XinRan","family":"Ning","sequence":"additional","affiliation":[]},{"given":"GuanFeng","family":"Wu","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55602-8_185"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005879229581"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005843632307"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(03)00040-3"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_23"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_22"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45422-5_23"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_23"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00368-5"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2007.07.004"},{"key":"ref4","first-page":"227","article-title":"Automatic deduction with hyper-resolution","volume":"3","author":"robinson","year":"1965","journal-title":"Internat J Computer Math 1"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/321607.321618"},{"key":"ref6","first-page":"1","article-title":"Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning","volume":"4","author":"slaney","year":"2016","journal-title":"Journal of Automated Reasoning"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1016\/0898-1221(76)90002-X"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/4.3.217"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80022-6"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0060630"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52885-7_106"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"ref20","first-page":"299","article-title":"Sine Qua non for large theory reasoning","volume":"6803","author":"voronkov","year":"2011","journal-title":"CADE 2011 LNCS"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-011-9168-1"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-009-9151-8"},{"key":"ref24","first-page":"1","article-title":"First-order theorem proving and vampire","volume":"8044","author":"voronkov","year":"2013","journal-title":"CAV 2013 LNCS"},{"journal-title":"TSTP Solution Domains","year":"2019","author":"sutcliffe","key":"ref23"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.3233\/AIC-160709"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.3233\/AIC-150668"}],"event":{"name":"2019 IEEE 14th International Conference on Intelligent Systems and Knowledge Engineering (ISKE)","start":{"date-parts":[[2019,11,14]]},"location":"Dalian, China","end":{"date-parts":[[2019,11,16]]}},"container-title":["2019 IEEE 14th International Conference on Intelligent Systems and Knowledge Engineering (ISKE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9163188\/9170202\/09170395.pdf?arnumber=9170395","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,18]],"date-time":"2022-07-18T15:19:21Z","timestamp":1658157561000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9170395\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11]]},"references-count":26,"URL":"https:\/\/doi.org\/10.1109\/iske47853.2019.9170395","relation":{},"subject":[],"published":{"date-parts":[[2019,11]]}}}