Conditional logics have a long history, and recently they have found several applications in artificial intelligence, such as deductive databases, nonmonotonic reasoning, belief revision. GoalDUCK is a theorem prover implementing a goal-directed proof procedure for the basic system of normal conditional logics CK. If you need some help, please contact: pozzato[at]di.unito.it or consult the user manual.