max planck institut
informatik
informatik
Kurzfassung:
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Kurzfassung:
Hybrid logic and modal logic with the difference
modality (MLD) are modal logics with equality.
Despite recent advances for hybrid logic, terminating
tableau systems for MLD have remained a challenge.
The established decision procedure [Balbiani and
Demri 1997] does not terminate for all inputs, and a
terminating tableau system for MLD with inverse
modalities was not known.
I will report about ongoing work with Mark Kaminski
and present a terminating tableau system for
a modal logic MLE that subsumes hybrid logic and MLD.
Our approach avoids the syntactic limitations of
modal logic by representing MLE as a fragment of
simple type theory. This way the connection between
MLE and pure predicate logic with equality (PLE)
becomes formal. PLE subsumes MLE up to translation,
and the terminating tableau system for MLE appears as
a refinement of a complete tableau system for PLE.
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Zusammenfassung:
We present a general framework which allows to identify complex theories
important in verification for which efficient reasoning methods exist.
The framework we present is based on a general notion of locality.
We show that locality considerations allow us to obtain parameterized
decidability and complexity results for many (combinations of) theories
important in verification in general and in the verification of parametric
systems in particular.
We give numerous examples; in particular we show that several theories
of data structures studied in the verification literature -- e.g.
various theories of pointer structures and of arrays -- can be seen as
local extensions of a base theory.
The general framework we use allows us to identify situations in which
some of the syntactical restrictions imposed in previous papers can be
relaxed.
(The talk is based on joint work with Carsten Ihlemann and Swen Jacobs.)
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Zusammenfassung:
Knowledge Compilation is a common technique for propositional logic
knowledge bases. The idea is to transform a given knowledge base into a
special normal form, for which queries can be answered efficiently. We
propose to apply this technique to knowledge bases defined in
Description Logic.
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Zusammenfassung:
We introduce a new rule-based formalism - OWL1.1 Rules - for knowledge
representation and reasoning for the Semantic Web. OWL1.1 Rules have the
following features:
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Die Folien zum Vortrag sind hier (+ Video). Copyright beim/bei den Autoren.
Zusammenfassung:
We present a new algorithm for reasoning in the description logic SHIQ, which
is the most prominent fragment of the Web Ontology Language OWL. The algorithm
is based on ordered binary decision diagrams (OBDDs) as a datastructure for
storing and operating on large model representations. We thus draw on the
success and the proven scalability of OBDD-based systems. To the best of
our knowledge, we present the very first algorithm for using OBDDs for
reasoning with general TBoxes.
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.
Die Folien zum Vortrag sind hier. Copyright beim/bei den Autoren.