BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Mining Human Proofs from Machine Proofs - Paulo Oliva (Queen Mary 
 University of London)
DTSTART:20170718T100000Z
DTEND:20170718T110000Z
UID:TALK73491@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:When recently investigating an intuitionistic fragment of Luka
 siewicz logic [1-4]\, we were able to discover several interesting theorem
 s of this logic by searching for valid equations in the algebra of hoops. 
 Our search for valid equations or counter-models was done using&nbsp\;prov
 er9 and mace4 (https://www.cs.unm.edu/~mccune/mace4/). In this talk I will
  describe some of the results obtained\, mainly around double negation tra
 nslations of the classical logic into the intuitionistic counter-part\, bu
 t also the process by which we managed to translate prover9 equational pro
 ofs into human readable (and hopefully understandable) proofs.Joint work w
 ith Rob Arthan.[1] R Arthan and P Oliva\, Negative translations for affine
  and Lukasiewicz logic\, under review (http://www.eecs.qmul.ac.uk/~pbo/pap
 ers/paper045.pdf)[2] R Arthan and P Oliva\, On pocrims and hoops\, Arxiv (
 https://arxiv.org/abs/1404.0816)[3] R Arthan and P Oliva\, On affine logic
  and Lukasiewicz logic\, Arxiv (https://arxiv.org/abs/1404.0570)[4] R Arth
 an and P Oliva\, Dual hoops have unique halving\,&nbsp\;McCune Festschrift
 \, LNAI 7788\, pp. 165-180\, 2013
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR