BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/1423
DTSTAMP:20240509T082219Z
SUMMARY:Resolution is NP hard to automate
DESCRIPTION:Speaker: Sreejata Kishor  Bhattacharya (TIFR)\n\nAbstract: \nA 
 proof system P is called automatizable if there is an algorithm A that\, g
 iven input a statement phi\, runs in time poly(s) and outputs a P-proof of
  phi of size at most poly(s)\, where s is the size of the shortest P-proof
  of phi. It had been a long-standing open problem to determine if resoluti
 on is automatizable. In a breakthrough result\, Atserias and Muller showed
  that automating resolution is NP hard. They construct a polynomial time c
 omputable transformation A that\, on input a CNF phi\, outputs an unsatisf
 iable CNF A(phi) such that:(i) If phi is satisfiable\, A(phi) has polynomi
 al sized resolution refutations(ii) If phi is not satisfiable\, A(phi) doe
 s not have any subexponential sized resolution refutationWe shall describe
  this construction.\n
URL:https://www.tcs.tifr.res.in/web/events/1423
DTSTART;TZID=Asia/Kolkata:20240510T160000
DTEND;TZID=Asia/Kolkata:20240510T170000
LOCATION:A-201 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR