Hans Kleine Büning Boeken

This volume features papers from the 11th International Conference on Theory and Applications of Satisfiability Testing (SAT 2008), which has evolved from a workshop in 1996 to an annual international conference. It serves as a platform for researchers exploring various aspects of the propositional satisfiability problem and its applications. For the first time, the conference took place in Asia, specifically at the Zhudao Guest House near Sun Yat-Sen University in Guangzhou, P. R. China. Many complex combinatorial problems can be represented as SAT problems, leading to advancements in both practical heuristics and theoretical insights applicable to a wide array of real-world challenges. Notably, significant verification issues in hardware and software can be reformulated as SAT problems, making SAT a crucial technology for ensuring secure and reliable systems. The conference topics encompass both practical and theoretical research on SAT and its applications, including proof systems, proof complexity, search algorithms, heuristics, algorithm analysis, hard instances, randomized formulas, problem encodings, industrial applications, solvers, tools, case studies, and empirical results. SAT is broadly defined, encompassing not only propositional satisfiability but also quantified Boolean formulas (QBF) and satisfiability modulo theories (SMT).

This account of propositional logic concentrates on the algorithmic translation of important methods, especially of decision procedures for (subclasses of) propositional logic. Important classical results and a series of new results taken from the fields of normal forms, satisfiability and deduction methods are arranged in a uniform and complete theoretic framework. The algorithms presented can be applied to VLSI design, deductive databases and other areas. After introducing the subject the authors discuss satisfiability problems and satisfiability algorithms with complexity considerations, the resolution calculus with different refinements, and special features and procedures for Horn formulas. Then, a selection of further calculi and some results on the complexity of proof procedures are presented. The last chapter is devoted to quantified boolean formulas. The algorithmic approach will make this book attractive to computer scientists and graduate students in areas such as automated reasoning, logic programming, complexity theory and pure and applied logic.

This book contains a carefully refereed selection of papers presented at the 1995 Annual Conference of the European Association for Computer Science Logic, CSL '95, held in Paderborn, Germany, in September 1995. The 27 revised full papers included were selected after two rounds of reviewing from a total of 74 submissions for presentation at the conference and present the state-of-the-art in the area. Among the topics addressed are temporal logics, rewriting systems, deduction, theorem proving, process algebra, linear logics, proof theory, formal languages, and others.

Klappentext„... Dieses Lehrbuch ... stellt die Grundlagen dieses Gebiets ausführlich und umfassend ... dar.“ P. Schmitt. Internationale Mathematische Nachrichten, Wien

Die Programmiersprache PROLOG hat in den letzten Jahren durch zahlreiche Anwendungen in Expertensystemen und der natürlichen Sprachverarbeitung an Bedeutung gewonnen. Im Gegensatz zu prozeduralen Programmiersprachen, in denen Verfahren zur Lösung eines Problems programmiert werden, besteht das Programmieren in PROLOG aus einer Beschreibung des Problems. Dies führt zu unterschiedlichen Methoden und Herausforderungen beim Programm-Design. Das Buch basiert auf Vorlesungen an der Universität Karlsruhe und reflektiert die dabei gewonnenen Erfahrungen. Zunächst werden einfache Programme und Konstrukte in PROLOG vorgestellt, um den Leser mit der Programmierweise vertraut zu machen. Nach einem Exkurs zu den Grundlagen der Logik folgt ein Kapitel zur Syntax, orientiert an C-Prolog. Anschließend wird der Ablauf der Lösungssuche in PROLOG behandelt, gefolgt von einer ausführlichen Darstellung der wichtigsten Built-in-Prädikate mit Beispielen. Die Anwendungen sind in zwei Bereiche gegliedert: kurze Beispiele zu Mengen, Parsern, Spielen, Logik und Mathematik sowie ein ganzes Kapitel über Expertensysteme. Dabei liegt der Fokus auf der Entwicklung einer Shell zur Implementierung von Expertensystemen. Im Anhang befindet sich das vollständige Programm für diese Entwicklungsumgebung, abgesehen von einem Modul zur Wissenserfassung.