Mo Khodadadi

We discuss modifications of the unrestricted blocking rule by means of additional side conditions and/or additional premises. The approach preserves the termination property of the calculus and reduces search space of tableau decision procedures based on the calculus. In the variation of tableau procedure which we consider, terms are immediately rewritten with respect to the equalities conjectured by the blocking rule.

The paper shows that the description logic SHOI has the finite model property and presents a tableau calculus with several refinements for reasoning in SHOI. A novelty of the calculus is non-standard rules for dealing with TBox and RBox statements. Whereas in existing tableau approaches two fixed rules are used for dealing with TBox and RBox statements, our tableau calculus uses a dynamically generated set
of refined rules. Using this approach has become practical because reasoners with… Show more

The paper shows that the description logic SHOI has the finite model property and presents a tableau calculus with several refinements for reasoning in SHOI. A novelty of the calculus is non-standard rules for dealing with TBox and RBox statements. Whereas in existing tableau approaches two fixed rules are used for dealing with TBox and RBox statements, our tableau calculus uses a dynamically generated set
of refined rules. Using this approach has become practical because reasoners with flexible sets of rules can be generated with the tableau prover generation prototype MetTeL. We also define and investigate variations of the unrestricted blocking mechanism in which equality reasoning is realised by ordered rewriting, and the application of the blocking rule is controlled by excluding its application to a fixed, finite set of individual terms. Reasoning with the unique name assumption and excluding ABox elements from the application of blocking can be seen as two separate instances of this technique. Experiments show the refinements lead to fewer rule applications and improved performance. Show less

The paper shows that the description logic SHOI has the finite model property and presents a tableau calculus with several refinements for reasoning in SHOI. A novelty of the calculus is nonstandard rules for dealing with TBox and RBox statements. Whereas in existing tableau approaches two fixed rules are used for dealing with TBox and RBox statements, our tableau calculus uses a dynamically generated set of refined rules. Using this approach has become practical because reasoners with flexible… Show more

The paper shows that the description logic SHOI has the finite model property and presents a tableau calculus with several refinements for reasoning in SHOI. A novelty of the calculus is nonstandard rules for dealing with TBox and RBox statements. Whereas in existing tableau approaches two fixed rules are used for dealing with TBox and RBox statements, our tableau calculus uses a dynamically generated set of refined rules. Using this approach has become practical because reasoners with flexible sets of rules can be generated with the tableau prover
generation prototype MetTeL. We also define and investigate variations of the unrestricted blocking mechanism in which equality reasoning is realised by ordered rewriting, and the application of the blocking rule is controlled by excluding its application to a fixed, finite set of individual terms. Reasoning with the unique name assumption and excluding ABox elements from the application of blocking can be seen as two separate instances of this technique. Experiments show the refinements lead to fewer rule applications and improved performance. Show less

This paper introduces MetTeL , a tableau prover generator producing Java code from the specification of a tableau calculus for a logical language. MetTeL is intended to provide an easy to use system for non-technical users and allow technical users to extend the generated
implementations.

Introduces MetTeL2, a tableau prover generator producing Java code from the specification of a logical syntax and a tableau calculus. It is intended to provide an easy to use system for non-technical users and allow technical users to extend the generated implementations.

This paper presents a labelled tableau approach for deciding interrogative-epistemic logics (IEL). Tableau calculi for these logics have been derived using a recently introduced tableau synthesis method. We also consider an extension of the framework for a setting
with questioning modalities over sequences of formulae called sequential questioning logic (SQL). We have implemented the calculi using two approaches. The rst implementation has been obtained with the tableau prover generation… Show more

This paper presents a labelled tableau approach for deciding interrogative-epistemic logics (IEL). Tableau calculi for these logics have been derived using a recently introduced tableau synthesis method. We also consider an extension of the framework for a setting
with questioning modalities over sequences of formulae called sequential questioning logic (SQL). We have implemented the calculi using two approaches. The rst implementation has been obtained with the tableau prover generation software MetTeL2, while the other implementation is a prover implemented in Haskell. Show less

This paper presents an abstract tableau calculus for the description logic SHOI. SHOI is the extension of ALC with singleton concepts, role inverse, transitive roles and role inclusion axioms. The presented tableau calculus is inspired by a recently introduced tableau synthesis framework. Termination is achieved by a variation of the unrestricted blocking mechanism that immediately rewrites terms with respect to the conjectured equalities. This approach leads to reduced search space for… Show more

This paper presents an abstract tableau calculus for the description logic SHOI. SHOI is the extension of ALC with singleton concepts, role inverse, transitive roles and role inclusion axioms. The presented tableau calculus is inspired by a recently introduced tableau synthesis framework. Termination is achieved by a variation of the unrestricted blocking mechanism that immediately rewrites terms with respect to the conjectured equalities. This approach leads to reduced search space for decision procedures based on the calculus. We also discuss restrictions of the application of the blocking rule by means of additional side conditions and/or additional premises. Show less

This paper introduces METTEL2 , a tableau prover generator producing JAVA code from the specifications of a logical syntax and a tableau calculus. It is intended to provide an easy to use system for non-technical users and allow technical users to extend the implementation of generated provers.

This paper presents three logical formalizations extending dynamic epistemic modal logic with multi-agent features. The first feature consists in considering interrogative components which are modelled by dynamic questioning modalities encoding model-changing operations. The multi-agent
aspects specific to these dynamic actions are captured using preconditions for executing questioning and resolution actions. The second feature consists in considering a special
kind of privacy of dynamic… Show more

This paper presents three logical formalizations extending dynamic epistemic modal logic with multi-agent features. The first feature consists in considering interrogative components which are modelled by dynamic questioning modalities encoding model-changing operations. The multi-agent
aspects specific to these dynamic actions are captured using preconditions for executing questioning and resolution actions. The second feature consists in considering a special
kind of privacy of dynamic actions. We formalise group opaque dynamic questioning effects via a new semantics accounting for the possibility that some agents are aware of interrogative-epistemic events taking place while other agents are oblivious to these events. The third feature extends the formalization to accommodate sequences of questioning actions. For all these logics we present sound and complete tableau calculi with the property that they can be used as finite model generators for any formulae with finite models. The presented calculi have been derived using
tableau synthesis methods. Show less

This paper presents the first systematic treatment of tableau calculi for modal logic K with global counting operators. Using a recently introduced tableau synthesis framework we establish two terminating tableau calculi for the logic. Whereas the first calculus is a prefix tableau calculus, the second is a refinement that internalises the semantics of the logic without using nominals. We prove the finite model property for the logic and show that adding the unrestricted blocking mechanism does… Show more

This paper presents the first systematic treatment of tableau calculi for modal logic K with global counting operators. Using a recently introduced tableau synthesis framework we establish two terminating tableau calculi for the logic. Whereas the first calculus is a prefix tableau calculus, the second is a refinement that internalises the semantics of the logic without using nominals. We prove the finite model property for the logic and show that adding the unrestricted blocking mechanism does not break soundness and completeness of the calculi and ensures termination in both cases. We have successfully implemented the prefix tableau calculus in the MetTeL tableau
prover generation platform. Show less

MetTeL is a generic tableau prover for various modal, intuitionistic, hybrid, description and metric logic. The core component of MetTeL is a logic-independent tableau inference engine. A novel feature is that users have the ability to flexibly specify the set of tableau rules to be used in derivations. Termination can be achieved via a generalisation of a standard loop checking mechanism or unrestricted blocking.

METTEL is a generic tableau prover for various modal, description, hybrid, intuitionistic and metric logics. The core component of METTEL is a logic-independent tableau inference engine. A novel feature is that users have the ability to specify the set of tableau rules to be used in derivations. Termination can be achieved via a generalisation of a standard loop checking mechanism, or
unrestricted blocking.