Auflistung nach:
Auflistung Künstliche Intelligenz 24(1) - März 2010 nach Erscheinungsdatum
1 - 10 von 16
Treffer pro Seite
Sortieroptionen
- ZeitschriftenartikelKünstliche Intelligenz ab 2010 bei Springer(KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010) Althoff, Klaus-Dieter
- ZeitschriftenartikelSmall is Again Beautiful in Description Logics(KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010) Baader, Franz; Lutz, Carsten; Turhan, Anni-YasminThe Description Logic (DL) research of the last 20 years was mainly concerned with increasing the expressive power of the employed description language without losing the ability of implementing highly-optimized reasoning systems that behave well in practice, in spite of the ever increasing worst-case complexity of the underlying inference problems. OWL DL, the standard ontology language for the Semantic Web, is based on such an expressive DL for which reasoning is highly intractable. Its sublanguage OWL Lite was intended to provide a tractable version of OWL, but turned out to be only of a slightly lower worst-case complexity than OWL DL. This and other reasons have led to the development of two new families of light-weight DLs, $\mathcal{EL}$ and DL-Lite, which recently have been proposed as profiles of OWL 2, the new version of the OWL standard. In this paper, we give an introduction to these new logics, explaining the rationales behind their design.
- ZeitschriftenartikelInstance Based Methods—A Brief Overview(KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010) Baumgartner, Peter; Thorstensen, EvgenijInstance-based methods are a specific class of methods for automated proof search in first-order logic. This article provides an overview of the major methods in the area and discusses their properties and relations to the more established resolution methods. It also discusses some recent trends on refinements and applications. This overview is rather brief and informal, but we provide a comprehensive literature list to follow-up on the details.
- ZeitschriftenartikelSpecial Issue on Automated Deduction(KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010) Giesl, Jürgen
- ZeitschriftenartikelDifferential Dynamic Logics(KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010) Platzer, AndréDesigning and analyzing hybrid systems, which are models for complex physical systems, is expensive and error-prone. The dissertation presented in this article introduces a verification logic that is suitable for analyzing the behavior of hybrid systems. It presents a proof calculus and a new deductive verification tool for hybrid systems that has been used successfully to verify aircraft and train control.
- ZeitschriftenartikelPractical Aspects of Automated Deduction for Program Verification(KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010) Ahrendt, Wolfgang; Beckert, Bernhard; Giese, Martin; Rümmer, PhilippSoftware is vital for modern society. It is used in many safety- or security-critical applications, where a high degree of correctness is desirable. Over the last years, technologies for the formal specification and verification of software—using logic-based specification languages and automated deduction—have matured and can be expected to complement and partly replace traditional software engineering methods in the future. Program verification is an increasingly important application area for automated deduction. The field has outgrown the area of academic case studies, and industry is showing serious interest. This article describes the aspects of automated deduction that are important for program verification in practise, and it gives an overview of the reasoning mechanisms, the methodology, and the architecture of modern program verification systems.
- ZeitschriftenartikeliQser GIN Plattform(KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010) Wurzer, JörgDie iQser GIN Plattform verwandelt den Rohstoff an Daten in verwertbare, praxisrelevante Informationen. In der Wikipedia heißt es: „Information ist […] Wissenstransfer beziehungsweise „Wissen in Aktion“. Information entsteht […] immer nur punktuell, wenn ein Mensch zur Problemlösung Wissen (eine bestimmte Wissenseinheit) benötigt.“ Genau diese Aufgabe übernimmt die iQser GIN Plattform durch die intelligente und dynamische Vernetzung von Daten, damit sie zu Informationen in einem Kontext werden.
- ZeitschriftenartikelDeductive Verification of System Software in the Verisoft XT Project(KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010) Beckert, Bernhard; Moskal, MichałThe main goal of the Verisoft XT project is the creation of methods and tools which allow for the pervasive formal verification of integrated computer systems, and the prototypical realization of four concrete industrial application tasks.In this paper, we report on two of Verisoft XT’s sub-projects, where formal verification is applied to real-world system software, namely Microsoft’s Hypervisor and the embedded operating system PikeOS. We describe the deductive verification technology used in Verisoft XT and the tool chain that implements these methods, including the C verifier called VCC and the SMT solver Z3.
- ZeitschriftenartikelNews(KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010)
- ZeitschriftenartikelLearning and Recognizing Structures in Façade Scenes (eTRIMS)—A Retrospective(KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010) Hotz, Lothar; Neumann, BerndScene interpretation is the task of automatically creating descriptions for images. Such descriptions typically contain not only primitive objects but also structures that constitute primitive and structured objects. The learning and recognition of such structures was the objective of the EU project “eTraining for the Interpretation of Man-made Scenes (eTRIMS)”. The retrospective at hand presents main results of this project.