Auflistung nach:
Auflistung Künstliche Intelligenz 24(1) - März 2010 nach Titel
1 - 10 von 16
Treffer pro Seite
Sortieroptionen
- ZeitschriftenartikelA SAT Solver for Circuits Based on the Tableau Method(KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010) Egly, Uwe; Haller, LeopoldWe present an extension of the BC tableau, a calculus for determining satisfiability of constrained Boolean circuits. We argue that a satisfiability decision procedure based on the BC tableau can be implemented as a non-clausal DPLL procedure and that therefore, advances to the DPLL framework can be integrated into such a tableau procedure. We present a prototypical implementation of these ideas and evaluate it using a set of benchmark instances. We show that the extensions increase the efficiency of the basic BC tableau considerably and compare the performance of our solver with that of the non-clausal solver NoClause and the CNF-based SAT solver MiniSat.
- ZeitschriftenartikelCurrent Trends in Automated Deduction(KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010) Giesl, JürgenAutomated deduction is one of the key areas in artificial intelligence. In this short article we give an overview on some of the main current research topics in automated deduction.
- 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.
- 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.
- 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.
- 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.
- ZeitschriftenartikelKünstliche Intelligenz ab 2010 bei Springer(KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010) Althoff, Klaus-Dieter
- 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.
- ZeitschriftenartikelLiSA: Auf dem Weg zur sicheren Assistenzrobotik(KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010) Schulenburg, Erik; Elkmann, Norbert; Fritzsche, Markus; Hertzberg, Joachim; Stiene, StefanDer vorliegende Projektbericht gibt einen Überblick über das Verbundprojekt „LiSA – Assistenzroboter in Laboren von Life-Science-Unternehmen“, das zwischen April 2006 und Juli 2009 im Rahmen der „Leitinnovation Servicerobotik“ vom Bundesministerium für Bildung und Forschung (BMBF) gefördert wurde. Im Rahmen des Projektes wurde ein komplexes Servicerobotersystem entwickelt und aufgebaut. Acht Verbundpartner aus Forschung und Industrie entwickelten neue Technologien und Systeme in den Bereichen Navigation, Bildverarbeitung und Multimodale Interaktion. Ein weiterer Schwerpunkt des Projektes war die Betrachtung von Sicherheitsaspekten und die Entwicklung entsprechender Komponenten, um einen gefahrlosen Betrieb von Assistenzrobotern zu gewährleisten. Ein wesentlicher Beitrag war dabei die Entwicklung einer künstlichen Haut für Serviceroboter, die orts- und kraftaufgelöst Berührungen erfassen und als Sicherheitssensor eingesetzt werden kann.
- ZeitschriftenartikelLogic-Based Question Answering(KI - Künstliche Intelligenz: Vol. 24, No. 1, 2010) Furbach, Ulrich; Glöckner, Ingo; Helbig, Hermann; Pelzer, BjörnQuestion answering systems aim to provide concise and correct responses to arbitrary questions, communicating with the user in a natural language. This way they help making the knowledge of large textual sources accessible in an intuitive manner which goes beyond the capabilities of conventional search engines. In the LogAnswer project the universities of Hagen and Koblenz cooperate to build a German language question answering system which combines computational linguistics and automated reasoning to deduce answers from a knowledge base derived from Wikipedia.