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
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.
- An online interface and some case studies is available at the MetTeL2 online demo page.
- The system description of MetTeL2 and other relevant publications are accessible at the papers page.
- MetTeL2 Download page
MetTeL1
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.
- A manual has been prepared for MetTeL1 which is available for download
- The system description for MetTeL1 published in the Proceedings of TABLEAUX11 is available via the papers page
- MetTeL1 download page
Contact
We welcome any comments or suggestions of our work. You may use the contact page for sending us your comments.
