MetTeL 2 online demo
Reading the system
description for MetTeL2 may help you in using the following tool.
1.Define the syntax of the logical theory in section 1 or select one of the predefined logics.
1. Syntax of logic and tableau formulas
You may select one of the predefined syntax for following
list:
User Defined syntax ...
Description logic ALBO plus identity
Description logic ALC with nominal support
Intuitionistic logic
Modal logic S4
Boolean logic
Simple Example for checking equality of list
Extension of list example with concatenation
Modal logic K with global counting operators (n=3)
Three-valued Lukasiewicz logic
2. Define properties (optional)
3. Logic's tableau calculus
New rule
Tableau calculus display:
There are no tableau rules
defined.
4. Prover for logic
Click the following button to generate the prover
Generate a prover base on my input
Here is some debugging information:
try the prover with this input
Notice: we do collect the usage data for internal performance test.
download the latest version
Compiled system of latest version can be downloaded here. For other version and example go to Download section ยป
