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	Büro Meynen, Gloria 29 February 2012 (has links) Den Namen »Büro« leitet die vorliegende Arbeit von den Überresten der Sumpfpflanze »eriophorum angustifolium« her, die auch Burra genannt wird. Im Mittelalter wurden aus den verwesten Fasern dieser Pflanze Rechentücher gewebt. Ausgehend von den Techniken und Praktiken der Buchhaltung und des Rechnens liegt der Schwerpunkt dieser Arbeit auf einer Geschichte der Routinen. Im ersten Teil leitet die Autorin die Techniken des deduktiven Beweisens von der Erfindung der ebenen Fläche ab. Mit den Techniken des Zeigens und Verweisens beschreibt sie die Anfänge der Abstraktion. Ein zweiter Teil wendet sich den Operationen der euklidischen Fläche zu. Ausgehend von der Etymologie der römischen Zahl X werden die Anfänge der Büroroutinen in den Operationen des Dezimierens, Abschlagens und in der Durchkreuzung gesucht. Mit ihnen konzentriert sich die Autorin auf die Techniken des Löschens und der Frage, wie man Zeichen in und auf der Fläche bewegen kann. Routinen werden als kleine Routen auf der Fläche aufgefasst, ihre Anfänge in den frühen Multiplikationsverfahren, einer Wissensgeschichte des Multiplikationszeichen X, in dem Zeilenvorschub und der doppelten Anschreibung der Posten in der doppelten Buchhaltung gesucht, die Luca Pacioli mit zwei gekreuzten Linien testiert. Das vorliegende Buch legt den Schwerpunkt auf die Kulturtechniken von Bild, Schrift und Zahl und kommt zu dem Schluss, dass das Büro im frühen 13. Jahrhundert ein neues operationales Wissen einführt. Es ist ein Ort, der der Gedächtniskultur der Erinnerung und Wiederholung ein Wissen der konstanten Zirkulation und Veränderung entgegensetzt. / The author traces the words »bureau« and »bureaucracy« back to the relics of eriophorum angustifolium, i.e. a marsh plant, that is also known under the colloquial name of »burra«. In the Middle Ages this plant was used as raw material for a portable abacus made of chunk wool. Starting from practices of counting and calculating this dissertation explores routines of office work. In the first part (A) the author argues that the practices and technics of diagrammatic reasoning depend on the invention of the plane surface. By exploring the routines of pointing and referring this part deals with the beginnings of abstraction. The second part (B), a media history of routines, takes a closer look at those operations that were performed on the plane surface. Starting from the etymology of the numeral X that the Romans used for operations of foiling and decimating, the author finds the origins of bureaucratic routines in techniques of erasure. Based on the thesis that routines are small routes on plane surfaces the author identifies the beginnings of bureaucratic operations in early multiplication algorithms, the operation sign x, and finally in the cancelling of posts in early double-entry bookkeeping. Thus, the second part of the dissertation closely relates the history of writing, spelling and accounting to the technics of erasing. By analysing the operations of writing, drawing and counting the author comes to the conclusion, that at the beginning of the 13th century the office is a place of new operational knowledge – it confronts a static memory culture of repetition and remembering with a mobile culture of circulation and constant change. Kulturtechniken Wissensgeschichte Gnomon Implizites Wissen Deduktives Beweisen Gnomon Media History Euclidean plane Implicit Knowing Diagrammatic reasoning 000 Allgemeines, Wissenschaft 01 Wissenschaft und Kultur allgemein AP 18000 ddc:000
4	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
5	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
6	Isomorphic Visualization and Understanding of the Commutativity of Multiplication: from multiplication of whole numbers to multiplication of fractions Malaty, George 16 March 2012 (has links) (PDF) No description available. Begriffe Relationen Probleme ikonisch dynamisch zweidimensional isomorph Visualisierung allgemeiner Fall Farbnutzung demonstrieren lösen darstellen beweisen verstehen Motivation Kommutativität der Multiplikation ganze Zahlen Brüche Einheitsbrüche Schulbuch Klassenraum concepts relations problems iconic dynamic 2-dimentional isomorphic visualisation general case colour-use demonstrate solve pose proof understanding motivation commutativity of multiplication whole numbers fractions unit fraction textbooks classroom ddc:510 rvk:SD 2011
7	Isomorphic Visualization and Understanding of the Commutativity of Multiplication: from multiplication of whole numbers to multiplication of fractions Malaty, George 16 March 2012 (has links) No description available. info:eu-repo/classification/ddc/510 ddc:510
8	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

Search results