{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T14:14:15Z","timestamp":1753884855384},"reference-count":16,"publisher":"World Scientific Pub Co Pte Lt","issue":"06","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Artif. Intell. Tools"],"published-print":{"date-parts":[[2006,12]]},"abstract":"<jats:p> Automated Theorem Proving (ATP) systems are complex pieces of software, and thus may have bugs that make them unsound. In order to guard against unsoundness, the derivations output by an ATP system may be semantically verified by trusted ATP systems that check the required semantic properties of each inference step. Such verification needs to be augmented by structural verification that checks that inferences have been used correctly in the context of the overall derivation. This paper describes techniques for semantic verification of derivations, and reports on their implementation and testing in the GDV verifier. <\/jats:p>","DOI":"10.1142\/s0218213006003119","type":"journal-article","created":{"date-parts":[[2006,12,15]],"date-time":"2006-12-15T06:50:55Z","timestamp":1166165455000},"page":"1053-1070","source":"Crossref","is-referenced-by-count":17,"title":["SEMANTIC DERIVATION VERIFICATION: TECHNIQUES AND IMPLEMENTATION"],"prefix":"10.1142","volume":"15","author":[{"given":"GEOFF","family":"SUTCLIFFE","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Miami, P. O. Box 248154, Coral Gables, FL 33124, USA"}]}],"member":"219","published-online":{"date-parts":[[2011,11,21]]},"reference":[{"key":"rf1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"rf2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021939521172"},{"key":"rf7","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004562"},{"key":"rf9","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"rf10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"rf11","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3188-0_16"},{"key":"rf14","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541"},{"key":"rf15","first-page":"79","volume":"15","author":"Pelletier F. J.","journal-title":"AI Communications"},{"key":"rf18","first-page":"91","volume":"15","author":"Riazanov A.","journal-title":"AI Communications"},{"key":"rf19","volume-title":"Handbook of Automated Reasoning","author":"Robinson A.","year":"2001"},{"key":"rf20","first-page":"383","volume":"3","author":"Rudnicki P.","journal-title":"Journal of Automated Reasoning"},{"key":"rf23","first-page":"111","volume":"15","author":"Schulz S.","journal-title":"AI Communications"},{"key":"rf28","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(01)00113-8"},{"key":"rf29","unstructured":"G.\u00a0Sutcliffe, J.\u00a0Zimmer and S.\u00a0Schulz, Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, Frontiers in Artificial Intelligence and Applications\u00a0112, eds. W.\u00a0Zhang and V.\u00a0Sorge (IOS Press, 2004)\u00a0pp. 201\u2013215."},{"key":"rf31","doi-asserted-by":"publisher","DOI":"10.1007\/BF00252178"},{"key":"rf33","doi-asserted-by":"publisher","DOI":"10.1145\/1039813.1039816"}],"container-title":["International Journal on Artificial Intelligence Tools"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218213006003119","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T12:55:37Z","timestamp":1565182537000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218213006003119"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,12]]},"references-count":16,"journal-issue":{"issue":"06","published-online":{"date-parts":[[2011,11,21]]},"published-print":{"date-parts":[[2006,12]]}},"alternative-id":["10.1142\/S0218213006003119"],"URL":"https:\/\/doi.org\/10.1142\/s0218213006003119","relation":{},"ISSN":["0218-2130","1793-6349"],"issn-type":[{"value":"0218-2130","type":"print"},{"value":"1793-6349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,12]]}}}