{"id":5444,"date":"2018-07-22T04:07:42","date_gmt":"2018-07-22T03:07:42","guid":{"rendered":"https:\/\/www.ciirc.cvut.cz\/?p=5444"},"modified":"2019-01-22T14:34:22","modified_gmt":"2019-01-22T13:34:22","slug":"ciirc-ctu-team-led-by-j-urban-won-in-automated-reasoning-competition","status":"publish","type":"post","link":"https:\/\/www.ciirc.cvut.cz\/cs\/ciirc-ctu-team-led-by-j-urban-won-in-automated-reasoning-competition\/","title":{"rendered":"T\u00fdm CIIRC \u010cVUT veden\u00fd Dr. J. Urbanem vyhr\u00e1l mistrovstv\u00ed sv\u011bta v automatick\u00e9m usuzov\u00e1n\u00ed"},"content":{"rendered":"<p style=\"text-align: left;\">Ve dnech 13. a 14. 7. 2018 se v Oxfordu na Federated Logic Conference (<a href=\"http:\/\/www.floc2018.org\/\">FLoC18<\/a>) konalo Mistrovstv\u00ed sv\u011bta v automatick\u00e9m dokazov\u00e1n\u00ed v\u011bt pro rok 2018 (<a href=\"http:\/\/www.cs.miami.edu\/~tptp\/CASC\/J9\/\">CASC-J9<\/a>). Byl to dvac\u00e1t\u00fd t\u0159et\u00ed ro\u010dn\u00edk t\u00e9to sout\u011b\u017ee, kter\u00e1 se kon\u00e1 ka\u017edoro\u010dn\u011b od roku 1996. V\u00edce ne\u017e dvacet syst\u00e9m\u016f od t\u00fdm\u016f z USA, Asie a Evropy sout\u011b\u017eilo v \u0161esti diviz\u00edch.<\/p>\n<p style=\"text-align: left;\">Ve dvou diviz\u00edch <a href=\"http:\/\/www.cs.miami.edu\/~tptp\/CASC\/J9\/WWWFiles\/DivisionSummary1.html\">zv\u00edt\u011bzily<\/a> syst\u00e9my vyv\u00edjen\u00e9 <a href=\"http:\/\/ai4reason.org\/members.html\">t\u00fdmem<\/a> CIIRC \u010cVUT pracuj\u00edc\u00edm na ERC projektu <a href=\"http:\/\/ai4reason.org\">AI4REASON<\/a> Dr. Josefa Urbana a jeho spolupracovn\u00edk\u016f. V divizi LTB (rozs\u00e1hl\u00e9 teorie) zv\u00edt\u011bzil syst\u00e9m &#8222;Machine Learner for Automated Reasoning&#8220; (<a href=\"https:\/\/github.com\/JUrban\/MPTP2\/tree\/master\/MaLARea\">MaLARea 0.6<\/a>) vyv\u00edjen\u00fd Urbanem a jeho kolegy. Tento syst\u00e9m vy\u0159e\u0161il o 16% v\u00edc z 5000 probl\u00e9m\u016f v t\u00e9to divizi ne\u017e dal\u0161\u00ed syst\u00e9m.\u00a0 V divizi THF (probl\u00e9my v logice vy\u0161\u0161\u00edho \u0159\u00e1du) zv\u00edt\u011bzil syst\u00e9m <a href=\"http:\/\/satallaxprover.org\/\">Satallax 3.2<\/a> vyv\u00edjen\u00fd Dr. Chadem Brownem a jeho kolegy. Tento syst\u00e9m vy\u0159e\u0161il o 14% v\u00edc z 500 probl\u00e9m\u016f v t\u00e9to divizi ne\u017e dal\u0161\u00ed syst\u00e9m.<\/p>\n<p style=\"text-align: left;\">Divize LTB obsahuje probl\u00e9my vznikaj\u00edc\u00ed ve velk\u00fdch projektech verifikace matematiky a softwaru. Tento rok to byly probl\u00e9my z projektu <a href=\"https:\/\/cakeml.org\/\">CakeML<\/a>, kter\u00fd vyv\u00edj\u00ed verifikovanou implementaci programovac\u00edho jazyka ML. Divize THF obsahuje v\u00fdb\u011br probl\u00e9m\u016f formulovan\u00fdch v logice vy\u0161\u0161\u00edho \u0159\u00e1du. To je jeden z nejb\u011b\u017en\u011bj\u0161\u00edch formalizm\u016f pou\u017e\u00edvan\u00fdch pro verifikaci velk\u00fdch matematick\u00fdch d\u016fkaz\u016f a komplikovan\u00e9ho softwaru.<\/p>\n","protected":false},"excerpt":{"rendered":"<p style=\"text-align: left;\">Ve dnech 13. a 14. 7. 2018 se v Oxfordu na Federated Logic Conference (<a href=\"http:\/\/www.floc2018.org\/\">FLoC18<\/a>) konalo Mistrovstv\u00ed sv\u011bta v automatick\u00e9m dokazov\u00e1n\u00ed v\u011bt pro rok 2018 (<a href=\"http:\/\/www.cs.miami.edu\/~...\n<\/p>\n","protected":false},"author":11,"featured_media":5622,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"inline_featured_image":false,"footnotes":""},"categories":[2],"tags":[],"class_list":{"0":"post-5444","1":"post","2":"type-post","3":"status-publish","4":"format-standard","5":"has-post-thumbnail","7":"category-featured"},"acf":[],"_links":{"self":[{"href":"https:\/\/www.ciirc.cvut.cz\/wp-json\/wp\/v2\/posts\/5444","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.ciirc.cvut.cz\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.ciirc.cvut.cz\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.ciirc.cvut.cz\/wp-json\/wp\/v2\/users\/11"}],"replies":[{"embeddable":true,"href":"https:\/\/www.ciirc.cvut.cz\/wp-json\/wp\/v2\/comments?post=5444"}],"version-history":[{"count":0,"href":"https:\/\/www.ciirc.cvut.cz\/wp-json\/wp\/v2\/posts\/5444\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.ciirc.cvut.cz\/wp-json\/wp\/v2\/media\/5622"}],"wp:attachment":[{"href":"https:\/\/www.ciirc.cvut.cz\/wp-json\/wp\/v2\/media?parent=5444"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.ciirc.cvut.cz\/wp-json\/wp\/v2\/categories?post=5444"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.ciirc.cvut.cz\/wp-json\/wp\/v2\/tags?post=5444"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}