Spelling suggestions: "subject:"automatisches beweisen"" "subject:"automatisches beweisend""
1 |
A linearized DPLL calculus with learningArnold, 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.
|
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.
|
3 |
Knowledge-Based General Game PlayingSchiffel, 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.
|
4 |
Knowledge-Based General Game PlayingSchiffel, 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
|
5 |
An Active Domain Node Architecture for the Semantic Web / Eine Knotenarchitektur mit aktivem Verhalten für das Semantic WebSchenk, Franz 21 November 2008 (has links)
No description available.
|
Page generated in 0.0946 seconds