As written in the title, my question is about the possibility of creating a program which, given hypothesis and thesis, tries in some ways to demonstrate the theorem and print to user if it is demonstrable.
In general it depends on the theory you are taking into account. For example, if you consider FOL (first order logic) then this problem is known to be unsolvable (Entscheidungsproblem), while if you consider propositional logic, then the answer is yes (being it decidable). More informations about decidability could be found here: https://en.wikipedia.org/wiki/Decidability_(logic)#Some_decidable_theories