does anyone know about a prover that implements a calculus that handles the transitive closure operator ? I'm wondering if there is any such prover based on description logic, mu-calculus or second-order logic. regards, Guillaume Hoffmann