Global ETD Search

1	A linearized DPLL calculus with learning Arnold, Holger January 2007 (has links) This paper describes the proof calculus LD for clausal propositional logic, which is a linearized form of the well-known DPLL calculus extended by clause learning. It is motivated by the demand to model how current SAT solvers built on clause learning are working, while abstracting from decision heuristics and implementation details. The calculus is proved sound and terminating. Further, it is shown that both the original DPLL calculus and the conflict-directed backtracking calculus with clause learning, as it is implemented in many current SAT solvers, are complete and proof-confluent instances of the LD calculus. / Dieser Artikel beschreibt den Beweiskalkül LD für aussagenlogische Formeln in Klauselform. Dieser Kalkül ist eine um Klausellernen erweiterte linearisierte Variante des bekannten DPLL-Kalküls. Er soll dazu dienen, das Verhalten von auf Klausellernen basierenden SAT-Beweisern zu modellieren, wobei von Entscheidungsheuristiken und Implementierungsdetails abstrahiert werden soll. Es werden Korrektheit und Terminierung des Kalküls bewiesen. Weiterhin wird gezeigt, dass sowohl der ursprüngliche DPLL-Kalkül als auch der konfliktgesteuerte Rücksetzalgorithmus mit Klausellernen, wie er in vielen aktuellen SAT-Beweisern implementiert ist, vollständige und beweiskonfluente Spezialisierungen des LD-Kalküls sind. SAT DPLL Klausellernen Automatisches Beweisen SAT DPLL Clause Learning Automated Theorem Proving Data processing Computer science
2	A linearized DPLL calculus with clause learning (2nd, revised version) Arnold, Holger January 2009 (has links) Many formal descriptions of DPLL-based SAT algorithms either do not include all essential proof techniques applied by modern SAT solvers or are bound to particular heuristics or data structures. This makes it difficult to analyze proof-theoretic properties or the search complexity of these algorithms. In this paper we try to improve this situation by developing a nondeterministic proof calculus that models the functioning of SAT algorithms based on the DPLL calculus with clause learning. This calculus is independent of implementation details yet precise enough to enable a formal analysis of realistic DPLL-based SAT algorithms. / Viele formale Beschreibungen DPLL-basierter SAT-Algorithmen enthalten entweder nicht alle wesentlichen Beweistechniken, die in modernen SAT-Solvern implementiert sind, oder sind an bestimmte Heuristiken oder Datenstrukturen gebunden. Dies erschwert die Analyse beweistheoretischer Eigenschaften oder der Suchkomplexität derartiger Algorithmen. Mit diesem Artikel versuchen wir, diese Situation durch die Entwicklung eines nichtdeterministischen Beweiskalküls zu verbessern, der die Arbeitsweise von auf dem DPLL-Kalkül basierenden SAT-Algorithmen mit Klausellernen modelliert. Dieser Kalkül ist unabhängig von Implementierungsdetails, aber dennoch präzise genug, um eine formale Analyse realistischer DPLL-basierter SAT-Algorithmen zu ermöglichen. Automatisches Beweisen Logikkalkül SAT DPLL Klausellernen automated theorem proving logical calculus SAT DPLL clause learning Data processing Computer science
3	Knowledge-Based General Game Playing Schiffel, Stephan 14 June 2012 (has links) (PDF) The goal of General Game Playing (GGP) is to develop a system, that is able to automatically play previously unseen games well, solely by being given the rules of the game. In contrast to traditional game playing programs, a general game player cannot be given game specific knowledge. Instead, the program has to discover this knowledge and use it for effectively playing the game well without human intervention. In this thesis, we present a such a program and general methods that solve a variety of knowledge discovery problems in GGP. Our main contributions are methods for the automatic construction of heuristic evaluation functions, the automated discovery of game structures, a system for proving properties of games, and symmetry detection and exploitation for general games. Künstliche Intelligenz General Game Playing Heuristik Automatisches Beweisen Symmetryerkennung artificial intelligence general game playing heuristics automatic theorem proving symmetry detection ddc:004 rvk:ST 300 Agent <Künstliche Intelligenz> Artificial Intelligence: AI Automatische Handlungsplanung Heuristik Spiel
4	Knowledge-Based General Game Playing Schiffel, Stephan 29 July 2011 (has links) The goal of General Game Playing (GGP) is to develop a system, that is able to automatically play previously unseen games well, solely by being given the rules of the game. In contrast to traditional game playing programs, a general game player cannot be given game specific knowledge. Instead, the program has to discover this knowledge and use it for effectively playing the game well without human intervention. In this thesis, we present a such a program and general methods that solve a variety of knowledge discovery problems in GGP. Our main contributions are methods for the automatic construction of heuristic evaluation functions, the automated discovery of game structures, a system for proving properties of games, and symmetry detection and exploitation for general games.:1. Introduction 2. Preliminaries 3. Components of Fluxplayer 4. Game Tree Search 5. Generating State Evaluation Functions 6. Distance Estimates for Fluents and States 7. Proving Properties of Games 8. Symmetry Detection 9. Related Work 10. Discussion info:eu-repo/classification/ddc/004 ddc:004
5	An Active Domain Node Architecture for the Semantic Web / Eine Knotenarchitektur mit aktivem Verhalten für das Semantic Web Schenk, Franz 21 November 2008 (has links) No description available. 004 Informatik Mathematics and Computer Science Wissensmanagement OWL Semantic Web Beschreibungslogik Hybrides automatisches Beweisen Semantic Web Event-Driven Architecture OWL Active Knowledge Base Intensional Updates Hybrid Reasoning Description Logic F-Logic 54.64 54.71 54.72

1

Page generated in 0.0617 seconds