{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,2]],"date-time":"2025-07-02T01:49:17Z","timestamp":1751420957148},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Two complementary AI methods are used to improve the strength of the AI\/ATP service for proving conjectures over the HOL Light and Flyspeck corpora. First, several schemes for frequency-based feature weighting are explored in combination with distance-weighted k-nearest-neighbor classifier.  This results in 16% improvement (39.0% to 45.5% Flyspeck problems solved) of the overall strength of the service when using 14 CPUs and 30 seconds. The best premise-selection\/ATP combination is improved from 24.2% to 31.4%, i.e. by 30%. A smaller improvement is obtained by evolving targetted E prover strategies on two particular premise selections, using the Blind Strategymaker (BliStr) system. This raises the performance of the best AI\/ATP method from 31.4% to 34.9%, i.e. by 11%, and raises the current 14-CPU power of the service to 46.9%.<\/jats:p>","DOI":"10.29007\/5gzr","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T22:59:05Z","timestamp":1516748345000},"page":"87-77","source":"Crossref","is-referenced-by-count":15,"title":["Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution"],"prefix":"10.29007","volume":"14","author":[{"given":"Cezary","family":"Kaliszyk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"11545","event":{"name":"PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T23:00:09Z","timestamp":1516748409000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/VZv6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/5gzr","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}