{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T07:58:24Z","timestamp":1730275104775,"version":"3.28.0"},"reference-count":18,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,11]]},"DOI":"10.1109\/iske.2017.8258793","type":"proceedings-article","created":{"date-parts":[[2018,1,15]],"date-time":"2018-01-15T17:47:01Z","timestamp":1516038421000},"page":"1-6","source":"Crossref","is-referenced-by-count":1,"title":["Multi-clause synergized contradiction separation based first-order theorem prover \u2014 MC-SCS"],"prefix":"10.1109","author":[{"given":"Jian","family":"Zhong","sequence":"first","affiliation":[]},{"given":"Feng","family":"Cao","sequence":"additional","affiliation":[]},{"given":"Guanfeng","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Xu","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Liu","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_49"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_23"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9143-8"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.3233\/AIC-160709"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45620-1_22"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/TFUZZ.2012.2236095"},{"key":"ref16","article-title":"Non-clausal multi-ary a-generalized resolution principle for a lattice-valued logic system","author":"xu","year":"2015","journal-title":"submitted to Logic Journal of the IGPL under review"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1142\/9789813146976_0078"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1142\/9789813146976_0081"},{"key":"ref4","article-title":"Miz AR 40 for Mizar 40","volume":"abs 1310 2805","author":"kaliszyk","year":"2013","journal-title":"CoRR"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_22"},{"journal-title":"Prove9 and Mae4 (2005–2010)","year":"2016","author":"mccune","key":"ref6"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"ref8","first-page":"79","volume":"15","author":"pelletier","year":"2002","journal-title":"The development of CASC AI Communications"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_1"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_24"},{"journal-title":"First-order reasoning in Yices 2","year":"2012","author":"cruanes","key":"ref1"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"}],"event":{"name":"2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE)","start":{"date-parts":[[2017,11,24]]},"location":"Nanjing","end":{"date-parts":[[2017,11,26]]}},"container-title":["2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8246022\/8258711\/08258793.pdf?arnumber=8258793","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,2,19]],"date-time":"2018-02-19T18:56:04Z","timestamp":1519066564000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8258793\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11]]},"references-count":18,"URL":"https:\/\/doi.org\/10.1109\/iske.2017.8258793","relation":{},"subject":[],"published":{"date-parts":[[2017,11]]}}}