We are investigating interval-based temporal extensions of terminological logics. These extensions allow to model temporally rich domains with a terminological approach. The first part of the paper presents the extension of known terminological logics by adding temporal operators on intervals and providing a new semantics. Reasoning on taxonomies of time-dependent concepts defined with these logics involves computing a subsumption relation. We briefly describe what is known about un/decidability of subsumption and incomplete algorithms, but the emphasis of this paper is on a translation from these logics into a first order logic with two sorts. The temporal subsumption problem is reduced to validity for a subset of formulae. This translation formalizes the known relation between terminological and predicate logics, extending it to interval-based temporal operators. Through the translation we show that subsumptions are recursively enumerable for a class of these logics having as temporal domain the set of intervals defined as ordered pairs of rational numbers. We also show how ordinary theorem provers can be used as semi-automatic tools to prove temporal subsumption.

A formalization of interval-based temporal subsumption in first order logic / C. Bettini (LECTURE NOTES IN COMPUTER SCIENCE). - In: Foundations of knowledge representation and reasoning / [a cura di] G. Lakemeyer, B. Nebel. - Berlin : Springer, 1994. - ISBN 9783540581079. - pp. 53-73 [10.1007/3-540-58107-3_4]

A formalization of interval-based temporal subsumption in first order logic

C. Bettini
Primo
1994

Abstract

We are investigating interval-based temporal extensions of terminological logics. These extensions allow to model temporally rich domains with a terminological approach. The first part of the paper presents the extension of known terminological logics by adding temporal operators on intervals and providing a new semantics. Reasoning on taxonomies of time-dependent concepts defined with these logics involves computing a subsumption relation. We briefly describe what is known about un/decidability of subsumption and incomplete algorithms, but the emphasis of this paper is on a translation from these logics into a first order logic with two sorts. The temporal subsumption problem is reduced to validity for a subset of formulae. This translation formalizes the known relation between terminological and predicate logics, extending it to interval-based temporal operators. Through the translation we show that subsumptions are recursively enumerable for a class of these logics having as temporal domain the set of intervals defined as ordered pairs of rational numbers. We also show how ordinary theorem provers can be used as semi-automatic tools to prove temporal subsumption.
Settore INF/01 - Informatica
1994
Book Part (author)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/242510
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? ND
social impact