# Towards a Reasoning Model for Context-aware Systems: Modal Logic and the Tree Model Property

@article{Limn2015TowardsAR, title={Towards a Reasoning Model for Context-aware Systems: Modal Logic and the Tree Model Property}, author={Yensen Lim{\'o}n and Everardo B{\'a}rcenas and Edgard Ben{\'i}tez-Guerrero and Carmen Mezura-Godoy}, journal={Res. Comput. Sci.}, year={2015}, volume={99}, pages={9-18} }

Modal logics forms a family of formalisms widely used as reasoning frameworks in diverse areas of computer science. Description logics and their application to the web semantic is a notable example. Also, description logics have been recently used as a reasoning model for context-aware systems. Most reasoning algorithms for modal (de- scription) logics are based on tableau constructions. In this work, we propose a reasoning (satisability) algorithm for the multi-modal Km with converse. The… Expand

#### Figures and Topics from this paper

#### One Citation

Depth-First Reasoning on Trees

- Computer Science
- Computación y Sistemas
- 2018

This paper proposes a satisfiability algorithm for the mu-calculus extended with converse modalities and interpreted on unranked trees based on a depth-first search and proves the algorithm to be correct (sound and complete) and optimal. Expand

#### References

SHOWING 1-10 OF 24 REFERENCES

Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability

- Computer Science
- J. Artif. Intell. Res.
- 2009

This paper starts exploring the idea of performing automated reasoning tasks in modal and description logics by encoding them into SAT, so that to be handled by state-of-the-art SAT tools; as with most previous approaches, this investigation from the satisfiability in Km. Expand

How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi

- Mathematics, Computer Science
- TOCL
- 2001

A bottom-up decision procedure for propositional modal logic K based on the inverse method that considerably simplifies all proofs and is competitive with many state-of-the-art implementations of K. Expand

BDD-based decision procedures for the modal logic K ★

- Computer Science
- J. Appl. Non Class. Logics
- 2006

BDD-based decision procedures for the modal logic K are described, inspired by the automata-theoretic approach, but they avoid explicit automata construction and compute certain fixpoints of a set of types — which can be viewed as an on-the-fly emptiness of the automaton. Expand

CoLoSS: The Coalgebraic Logic Satisfiability Solver

- Computer Science, Mathematics
- Electron. Notes Theor. Comput. Sci.
- 2009

CoLoSS, the Coalgebraic Logic Satisfiability Solver, decides satisfiability of modal formulas in a generic and compositional way and synthesises decision procedures for modular combinations of logics that include the fusion of two modal logics as a special case. Expand

Why is Modal Logic So Robustly Decidable?

- Computer Science
- Descriptive Complexity and Finite Models
- 1996

It is argued that the robust decidability of modal logic can be explained by the so-called tree- model property, and it is shown how the tree-model property leads to automata-based decision procedures. Expand

Modal Satisfiability via SMT Solving

- Mathematics, Computer Science
- Software, Services, and Systems
- 2015

This work proposes a framework for obtaining decision procedures by adding instantiation rules to standard SAT and SMT solvers, and proves soundness, completeness, and termination of the procedures can be proved in a uniform and elementary way for the basic modal logic and some extensions. Expand

Query Reasoning on Trees with Types, Interleaving, and Counting

- Mathematics, Computer Science
- IJCAI
- 2011

This work considers the problem of query containment in the presence of type constraints for a class of regular path queries extended with counting and interleaving operators, and provides a logic-based framework supporting these operators which can be used to solve common query reasoning problems such as satisfiability and containment of queries in exponential time. Expand

Optimizing Description Logic Subsumption

- Mathematics, Computer Science
- J. Log. Comput.
- 1999

Effective optimization techniques can make a dramatic difference in the performance of knowledge representation systems based on expressive description logics and difficult problems in propositional modal logic can be effectively solved using the same techniques. Expand

Global Numerical Constraints on Trees

- Computer Science
- Log. Methods Comput. Sci.
- 2014

It is proved that the logic introduced in the present work is decidable in single exponential time even if the numerical constraints are in binary form, which implies a characterization of decidable counting extensions of XPath queries and XML schemas. Expand

MSPASS: Subsumption Testing with SPASS

- Computer Science
- Description Logics
- 1999

mspass is an enhancement of the rst-order theorem prover spass 17; 18; 19; 20] with a translator of modal formulae, formulae of description logics, and formulae of the relational calculus into… Expand