skip to content

Mining Human Proofs from Machine Proofs

Presented by: 
Paulo Oliva Queen Mary University of London, Queen Mary University of London
Tuesday 18th July 2017 - 11:00 to 12:00
INI Seminar Room 2
When recently investigating an intuitionistic fragment of Lukasiewicz logic [1-4], we were able to discover several interesting theorems of this logic by searching for valid equations in the algebra of hoops. Our search for valid equations or counter-models was done using prover9 and mace4 ( In this talk I will describe some of the results obtained, mainly around double negation translations of the classical logic into the intuitionistic counter-part, but also the process by which we managed to translate prover9 equational proofs into human readable (and hopefully understandable) proofs.

Joint work with Rob Arthan.

[1] R Arthan and P Oliva, Negative translations for affine and Lukasiewicz logic, under review (
[2] R Arthan and P Oliva, On pocrims and hoops, Arxiv (
[3] R Arthan and P Oliva, On affine logic and Lukasiewicz logic, Arxiv (
[4] R Arthan and P Oliva, Dual hoops have unique halving, McCune Festschrift, LNAI 7788, pp. 165-180, 2013
The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons