 Logic and Proof examination paper of the University of Oxford (2015)

The four-page University of Oxford Finals computer science examination held on 10 June 2015, Trinity Term 2015. Public primary-source archive: Lawrence Attachment.zip, member 2015-landp.pdf. Printed p. 4, Question 3(d), permits an arbitrary quantifier-free formula in an asserted least Herbrand model equivalence; that assertion fails when negative atoms are allowed, even for a satisfiable Horn clause.