cl-ch27-provlogic.pdf