Chatbots are intelligent agents with which users can hold conversations, usually via text or voice. In recent years, chatbots have become popular in businesses focused on client service. Despite an increasing interest for chatbots in education, clear information on how to design them as intelligent tutors has been scarce. This paper presents a formal methodology for designing and implementing a chatbot as an intelligent tutor for a university level course. The methodology is built upon first-order logic predicates which can be used in different commercially available tools, and focuses on two phases: knowledge abstraction and modelling, and conversation flow. As main result of this research, we propose mathematical definitions to model conversation elements, reasoning processes and conflict resolution to formalize the methodology and make it framework-independent.