Welcome to the MetTeL Home Page!

On this website we will make available tools and material related to our research into generating tableau calculi and implemented tableau provers.


MetTeL2 is complete reimplementation of MetTeL for the purpose of generating the implemented tableau provers. Using MetTeL2, user can define syntax of logical operators and tableau rules to be used.


MetTeL1 is a logic-independent inference engine, in which the user can specify tableau rules to be used. It is also the first tableau prover for the description logic ALBOid.


We welcome any comments or suggestions of our work. You may use the contact page for sending us your comments.