Quick Start

 

A tableau calculus and a problem set are the inputs required to run METTEL. The tableau calculus can be either selected from one of general predefined calculi mentioned in Section 4.2 ; or can be defined as explained in Section 4.1 and then given toMETTEL via an input file using the −tbl option.
The problem set can be either given to the system in an input file using the option −i or through the standard input stream. Input from standard input stream needs to be terminated by Ctrl + D.
The command for running METTEL has the following form:

java −jar mettel.jar
[−tbl <calculus−file−name> | <predefined tableau option> ]
[−o <output−file−name>]
[−e <error−file−name>]
[−i <problem−set−file−name>]

problem set in standard input if no input given Table 5.1 demonstrates different ways of running METTEL via the command line. The following example uses the predefined tableau calculus for Classical propositional logic (option −bool) for testing the satisfiability of P & Q &~P.

java −jar mettel.jar −bool
P & Q
~ P
(CTRL +D)

The output for this example is Unsatisfiable. This means the given formula was found to be unsatisfiable using the in-built tableau calculus of classical propositional logic. The output is going to be Satisfiable when the problem set is satisfiable with respect to the calculus. Section 8, gives more examples of running METTEL. There are errors that can terminate the execution of METTEL such as insufficient argument. As an example, if we use −i option when running METTEL, it should immediately follows by the file-name that contains the formulae for the problem set. Otherwise, METTEL prompts the user with the following message:

Input file name required

Chapter 7 describes the different kinds of errors that might occur when running METTEL.

System Overview

 

METTEL is a tableau prover for various modal, intuitionistic, hybrid, description and metric logics. The user has the option of using one of the several predefined tableau calculi or defines their own tableau calculus as input. METTEL implements generic loop-checking mechanisms and the unrestricted blocking mechanism to enforce termination. This makes METTEL useful for experimenting and testing tableau calculi for non-classical logics for which no sound and complete tableau calculi are known or for which no implementation exists.
METTEL decides the following logics:

• Classical propositional logic
• Intuitionistic propositional logic
• Hybrid logic HL(@, u) with the universal modality
• The logic MT of metric and topology
• All sublogics of the description logic ALBOid

At the moment, METTEL is the only tableau prover that can decide logics of metric and topology and description logics with role negation [5]. Using the facility to specify tableau rulesMETTEL can be used as a prover for many other more expressive or even undecidable logics.
As shown in Figure 1.1, METTEL takes a tableau calculus and a problem set as input. The tableau calculus is given by a set of tableau rules and the problem set is given by a set of formulae. The prover outputs Unsatisfiable if the set of formulae is not satisfiable with respect to the tableau calculus. The prover outputs Satisfiable and a model found for the set of formulae satisfiable with respect to the tableau calculus.

MetTeL Language

 

The language of METTEL is a many-sorted language. Namely, It consists of five sorts: formulae, nominal terms (including Skolem terms), attributes, rational parameters from metric logic and relational formulae (or roles).

 

2.1 Formulae

The primitives and operators that can be used to form formulae from other formulae, roles, attributes and nominals are shown in Table 2.1. The first column gives the names of the primitives and operators. The second column shows how these primitives and operators can be used to build formulae syntax in METTEL. The third and fourth columns give examples of both formulae in METTEL syntax and standard syntax from literature. The priority of the operators is as follows "forall, exists, @, false, true, ~, <<, &, |, −> and <−> ". Within METTEL formula, the first argument of box and diamond which is role, always appear within a pair of curly brackets, e.g. {Role}.

 

2.2 Nominals

In METTEL, nominals have one of the two forms as indicated in Table 2.2. The second column specifies their syntax and the third column gives examples.
By default, nominal symbols denote constants in the problem set and variables in the tableau calculus definition. They can be declared as being constant at the beginning of the tableau calculus definition, using the constant keyword.
constant: i, j ;
Nominal symbols can be declared as being variables at the beginning of the problem set, using variable keyword.
variable: i, j ;
We use lower-case identifiers for nominals to distinguish them from propositional variables, which should be specified by upper-case identifiers.

 

2.3 Attributes

The attributes sort in METTEL consists of an attribute which declared by a lower-case identifier. Table 2.3 contain the syntax and an example for attributes.

 

2.4 Parameters

Table 2.4 shows what primitives and operators we do allow in METTEL parameter. The first column shows that, parameters in METTEL are either constant or variable or the result of sum operator on two other parameters. The second column shows how these parameters can be written. Finally, the last column demonstrate a sample of these primitives and operators in METTEL syntax.

 

2.5 Role or Relational terms

Table 2.5 defines the syntax for role or relational formulae. The first column gives the names of the primitives and operators. The second column shows how these primitives and operators can be used to build role syntax in METTEL. The third and fourth columns give examples of both formulae in METTEL syntax and standard syntax from literature. The last three rows of Table 2.5 contain the roles for metric logic.
The priority of operators is as follows "+, |, &, ||, ., ;, *, ~, − and ^".
Since variable roles and propositional variables have the same syntax,METTEL distinguish them based on the context. Constant roles can be specified by lower-case identifiers.

Problem Set Definition

 

A problem set is a set of formulae. METTEL attempts to determine the satisfiability of the given problem set by applying the rules of a particular tableau calculus. The user can provide the problem set either in the standard input or in a file. Here are three examples of formulae specifiable in METTEL:

box box{~(~R | S)} FALSE
( @i dia{R} j & @j dia{R} k ) −> @i dia{R} k
exists{a$lt;x;a<y} P −> exists{a<(x+y)} P

The first formula encodes role inclusion R S in terms of the box operator, role negation and role union. The second formula defines R as a transitive relation in terms of the diamond operator, formula conjunction and formula implication. The last formula expresses the triangle property of metric relations (if there is a path to a property P consisting of two distances for an attribute a which are strictly less than x and y respectively, then there is an a-distance to P which is strictly less than x + y).
By default, nominals are constants. For using nominals as variables, they need to be declared as being variable at the beginning of the problem set as follows.
variable: i , k ;
The BNF specification of problem set is given in Figure 3.1.

Tableau Calculus Specification

 

The user can either choose one of the predefined tableau calculi, or define a new calculus in the tableau specification language of METTEL.

 

4.1 User-defined tableau calculus

The syntax for specifying tableau rules follows the standard premises/conclusions notation found in the literature.
Premises / Conclusion ; That is, premises and conclusions are separated by / and each rules is terminated by ;. There are three types of tableau rules: non-branching rules, branching rules and closure rules. Non-branching rules have only one branch in their conclusion. All the conclusion formulae used to be placed within a pair of brackets, as follows:
RulePremises / { RuleConclusion } ; Branching rules are the rules that split the current branch into more than one branch. A separated pair of curly brackets is required for each branch. The user can also optionally put a | between each branch for better readability. In general branching rules look like this:
RulePremises / { FirstConclusion } | ... | { LastConclusion } ; Finally, closure rules have FALSE in their conclusion. They have the following form: RulePremises / { FALSE }; Formally, the tableau specification input is defined by the BNF grammar given in Figure 4.1. Here, formula refers to any formula in METTEL syntax as defined in Table 2.1. Examples are shown in Table 4.1. On the left, the rules are written in METTEL syntax and on the right they are written in standard syntax found in the literature.


The first rule in Table 4.1 is an or rule, defined as a branching rule which creates a splitting point adding @i P to the left branch and @i Q to the right branch. The other rules are non-branching rules except the last rule which is a closure rule and has FALSE in the conclusion. The second rule is an instance of the standard and rule. It extends the current branch by adding both @i ~P and @i ~Q . We use comma to separate the formulae in one branch. The third rule is the standard box rule rewritten in terms of the negated diamond. The fourth rule is a standard diamond rule which generate a new nominal in the conclusion.The last rule, as we said earlier, is a closure rule.
Note the use of the Skolem term f[i,R,P] in the fourth rule. f is a fucntion name which is applied to a set of arguments. Here, f[i,R,P] represents a nominal newly created as witness for the premise @i dia{R} P. The arguments i,r,p given uniquely link the term to the premise (as i,r,p are the symbols occurring in the premise). Using Skolem terms in this way means that it is possible to see how nominals created. For example it can be read off from the term f[ f[a,r1,p],r2,q] that it represents a world reachable from world a via a r1 transition followed by a r2 transition. It also used, since it is easy to track the ancestors of any newly generated nominal.
Since role and propositional variable have similar syntax, we require the user to specify the sorts of arguments when a Skolem function is used for the first time. In the Skolem term, sort specification has the form of SORT:ARGUMENT for each argument, e.g., f[role: R,prop:P,nominal:i]. The sort can be param for parameter, attr for attribute, nom for nominal, prop for propositional and role for relation. So, the fourth rule of Table 4.1 would actually have to be written as f[nom:i, role:R, prop:P].
METTEL assumes the following conventions. In the user defined tableau, all the nominals are variable nominals unless they have been declared as constant nominal. Any constant nominals declaration should precise the rules.
constant: i , k ;
By default, constant roles are denoted by identifiers which starting with a lower-case letter, e.g. r. Constant roles cannot be substituted with any other role. Therefore, in rules, any constant role can only be matched to itself.

 

Rule application priority

METTEL group the provided rules in two three groups: 1.Non-branching, 2.Non- Branching and generating new nominal and 3.branching rules. Rules are applied in this order. The order in which rules inside a group are applied is determined by the order in which the rules are defined in the input file.

 

Switching off preprocessing

By default, METTEL does some preprocessing on the user-defined tableau calculus. This may sometimes result in unexpected behaviour. The preprocessing stage can be omitted usingthe −tbl−npp option instead of −tbl for inputting the tableau calculus. Therefore, the command for running METTEL will be as follows:
java −jar mettel.jar [−tbl−npp <t−fname>] [−i <in−fname>]

 

4.2 Predefined Tableau Calculi

There are several predefined tableau calculi in METTEL. All these tableau calculi are sound, complete and decision procedure for their targeted logic. For using these calculi, METTEL needs to be run with the appropriate option as listed in Table 4.2. Command line execution is via:
> java −jar mettel.jar [<tableau option>] [−i <in−fname>]
More information about running METTEL can be found in Section 5. In the remainder of this section, we provide the preprocessing that applies on problem sets beside the tableau rules for each calculus.

Running MetTeL

 

The input to MetTeL is a tableau calculus specification and a problem set. The tableau calculus can be either selected from one of the predefined calculi, mentioned in Section 4.2, or can be defined as explained in Section 4.1, and then gives to MetTeL in an input file. The problem set can be either provided to the system in an input file or through the standard input. The user needs to specify the end of the input from standard input stream by Ctrl + D.
Table 5.1 shows the different possibilities of running MetTeL.

MetTeL Output

 

METTEL is a refutation prover. This means when it outputs the unsatisfiable, the input problem is unsatisfiable with respect to the tableau calculus used. More precisely, when METTEL has constructed a closed tableau derivation, that is, in each branch a contradiction was found, METTEL outputs unsatisfiable. As an example, assume we have stored the sample tableau rules from Section 4.1 in the file sampleTableau.t.mtl and execute the following command:

> java −jar mettel.jar −tbl sampleTableau.t.mtl
box{R}(Q&P) & dia{R}~Q

METTEL produces the output: Unsatisfiable.
On the other hand, when the input problem is satisfiable with respect to the tableau calculus, it outputs satisfiable. More precisely, when METTEL has constructed an open tableau derivation, that is, one complete branch without contradiction, METTEL outputs satisfiable. If we run METTEL again with the same calculus but input box{R}(Q&P)& dia{R}P as problem set the output is:

Satisfiable

MODEL:[(@{f(n0,R,P)}P), (@{n0}(exists{R}f(n0,R,P))), (@{f(n0,R,P)}(~((~Q) |(~P)))), (@{n0}(~((exists{R}((~Q)|(~P))) |(~(exists{R}P))))), (@{n0 }(~(exists{R}((~Q)|(~P))))), (@{n0}(exists{R}P)), (@{f(n0,R,P)}Q)]

Compact Representation:[(@{f(n0,R,P)}P), (@{n0}(exists{R}f(n0,R,P))), (@{ f(n0,R,P)}Q)]

As can be seen in this example beside Satisfiable message, METTEL presents a model both in long and compact format. The provided model is the set of formulae which are produced by the application of the rules on the given problem set branch and did not result in closure.
Both the model and its compact representation are specified within a pair of square brackets. In the METTEL present nominals nominals are presented within a pairs of curly brackets in the output syntax.
In this example, in order to satisfy dia{R}P, METTEL creates a new nominal, namely the Skolem term {f(n0,R,P)}, which belong to P that is (@{f(n0,R,P)}P). This nominal then connects to the root nominal which is captured by @{n0}(exists{R}f(n0,R,P)). Then box rule is applied and Q & P is added to the newly generated nominal, that is @{f (n0,R,P)}(~((~Q)|(~P))). Since P is already true at this nominal, METTEL only adds Q to the set of formula true at this nominal, this is captured by (@{f(n0,R,P)}Q).
Since every model can be represented only by nominals, relations and propositions that are correct on them, METTEL also generates a Compact Representation of the model. This is done by selecting all the grounded literals.
Both output models follow the standard notation of prover outputs, which is responsible for the large number of parentheses and brackets.
By default,METTEL prints the output on the standard output. The output can be sent to a file by using option −o followed by the desired output file name when running METTEL.

java −jar mettel.jar −bool −i prob1.p.mtl −o result−probset1.p.mtl

The execution of METTEL can be terminated by pressing CTRL+C.

MetTeL Errors

 

When the execution of MetTeL aborts, this maybe be due to the following errors: unexpected tokens, unexpected character and insufficient argument.

7.1 Unexpected token

When parsing a user-defined tableau file or problem set, if MetTeL parse a word that is unexpected according to the BNF grammars provided in Figure 3.1 and Figure 4.1, it will throw an Unexpected token exception. The error message printed to standard output has the form:

== Unexpected token <source> ===========
(<line>:<column>) unexpected token: <token>
<extra information>
========================================

Here, <source> specifies where the error happened which can be either in the user defined tableau calculus or in the problem set. The second line specifies the position of the unexpected token and the token itself. In some cases, MetTeL provides some extra information to help the user find and rectify the error. For example, the following error message caused by attempting to specify a constant nominal in the problem set.

== Unexpected token Problem set ====================
(1:1) unexpected token: CONSTANT
CONSTANT can be only used at the beginning of tableau definition.
====================================================

7.2 Unexpected character

 

7.3 Missing argument

There are options that need to be followed by an argument. As an example, if we use −tbl option when running MetTeL, it should immediately followed by the name of a file that contains the specification of the tableau calculus. Otherwise, MetTeL gives the following error message:
Tableau file name required
The user should then run MetTeL again and supply all the required arguments. Options such as −i, −tbl−npp, −o and −e similarly need to be followed by an argument. They should be followed by file name for the problem set, file name for the user specified tableau calculus, desired file names for keeping the output and errors. If no argument is given, an error message is displayed.

MetTeL Examples

 

UPDATING ...

Download PDF version