We created a transformation language called ATL that can be used to define facts and rules in a convenient way also suitable for non-programmers. We show how this can be combined with a semantic tableau method to generate proofs, where the facts define axioms and the rules define theories. The semantic tableau method we use is extended with equivalence classes in order to provide automatic unification. The resulting proof system is powerful but still transparant and easy to use since the axioms and theories are defined in the user's own notation.