Automated Verification of Behavioural Properties of Prolog Programs