This volume contains the papers presented at the 11th International Conference on Theory and Applications of Satis?ability Testing (SAT 2008). The series of International Conferences on Theory and Applications of S- is?ability Testing (SAT) has evolved from a ?rst workshop on SAT in 1996 to an annual international conference which is a platform for researchers studying various aspects of the propositional satis?ability problem and its applications. In the past, the SAT conference venue alternated between Europe and North America. For the ?rst time, the conference venue was in Asia, more precisely at the Zhudao Guest House, near Sun Yat-Sen University in Guangzhou, P. R. China. Many hard combinatorial problems can be encoded into SAT. Therefore - provementsonheuristics onthe practicalside, as wellastheoreticalinsightsinto SAT apply to a large range of real-world problems. More speci?cally, many - portant practical veri?cation problems can be rephrased as SAT problems. This applies to veri?cation problems in hardware and software. Thus SAT is bec- ing one of the most important core technologies to verify secure and dependable systems. The topics of the conference span practical and theoretical research on SAT and its applications and include but are not limited to proof systems, proof complexity, search algorithms, heuristics, analysis of algorithms, hard instances, randomized formulae, problem encodings, industrial applications, solvers, s- pli?ers, tools, case studies, and empirical results. SAT is interpreted in a rather broad sense: besides propositional satis?ability, it includes, for example, the - main of quanti?ed Boolean formulae (QBF) and satis?ability modulo theories (SMT)

This volume presents the proceedings of the Computer Science Logic Workshop CSL '92, held in Pisa, Italy, in September/October 1992. CSL '92 was the sixth of the series and the first one held as Annual Conference of the European Association for Computer Science Logic (EACSL). Full versions of the workshop contributions were collected after their presentation and reviewed. On the basis of 58 reviews, 26 papers were selected for publication, and appear here in revised final form. Topics covered in the volume include: Turing machines, linear logic, logic of proofs, optimization problems, lambda calculus, fixpoint logic, NP-completeness, resolution, transition system semantics, higher order partial functions, evolving algebras, functional logic programming, inductive definability, semantics of C, classes for a functional language, NP-optimization problems, theory of types and names, sconing and relators, 3-satisfiability, Kleene's slash, negation-complete logic programs, polynomial-time oracle machines, and monadic second-order properties.

This volume presents the proceedings of the workshop CSL '91 (Computer Science Logic) held at the University of Berne, Switzerland, October 7-11, 1991. This was the fifth in a series of annual workshops on computer sciencelogic (the first four are recorded in LNCS volumes 329, 385, 440, and 533). The volume contains 33 invited and selected papers on a variety of logical topics in computer science, including abstract datatypes, bounded theories, complexity results, cut elimination, denotational semantics, infinitary queries, Kleene algebra with recursion, minimal proofs, normal forms in infinite-valued logic, ordinal processes, persistent Petri nets, plausibility logic, program synthesis systems, quantifier hierarchies, semantics of modularization, stable logic, term rewriting systems, termination of logic programs, transitive closure logic, variants of resolution, and many others.

The workshop Computer Science Logic '90 was held at the Max-Planck-Haus in Heidelberg, Germany, October 1-5, 1990. It was the fourth in a series of worskhops, following CSL '89 at the University of Kaiserslautern (see LNCS 440), CSL '88 at the University of Duisberg (see LNCS 385), and CSL '87 at the University of Karlsruhe (see LNCS 329). This volume contains 24 papers, chosen by means of a review procedure from the 35 papers presented at the workshop, some of which were invited and some selected from a total of 89 submissions. The papers cover a wide range of topics arising from the applications of logic to computer science.

This volume contains the revised versions of 28 papers presented at the third workshop on Computer Science Logic held in Kaiserslautern, FRG, October 2-6, 1989. These proceedings cover a wide range of topics both from theoretical and applied areas of computer science. More specifically, the papers deal with problems arising at the border of logic and computer science, e.g. in complexity, data base theory, logic programming, artificial intelligece, and temporal logic. The volume should be of interest to all logicians and computer scientists working in the above field.

This volume contains the papers which were presented at the second workshop "Computer Science Logic" held in Duisburg, FRG, October 3-7, 1988. These proceedings cover a wide range of topics both from theoretical and applied areas of computer science. More specifically, the papers deal with problems arising at the border of logic and computer science: e.g. in complexity, data base theory, logic programming, artificial intelligence, and concurrency. The volume should be of interest to all logicians and computer scientists working in the above fields.

This volume contains the papers which were presented to the workshop "Computer-Science Logic" held in Karlsruhe on October 12-16, 1987. Traditionally Logic, or more specifically, Mathematical Logic splits into several subareas: Set Theory, Proof Theory, Recursion Theory, and Model Theory. In addition there is what sometimes is called Philosophical Logic which deals with topics like nonclassical logics and which for historical reasons has been developed mainly at philosphical departments rather than at mathematics institutions. Today Computer Science challenges Logic in a new way. The theoretical analysis of problems in Computer Science for intrinsic reasons has pointed back to Logic. A broad class of questions became visible which is of a basically logical nature. These questions are often related to some of the traditional disciplines of Logic but normally without being covered adequately by any of them. The novel and unifying aspect of this new branch of Logic is the algorithmic point of view which is based on experiences people had with computers. The aim of the "Computer-Science Logic" workshop and of this volume is to represent the richness of research activities in this field in the German-speaking countries and to point to their underlying general logical principles.

Die Ausgangsbasis fiir die Erstellung dieses Buches waren Vorlesungen iiber Grundlagen wissensbasierter Systeme und iiber Deduktionssysteme. Ein zen- trales Thema dieser Veranstaltungen ist die Frage, inwieweit und mit wel- chen Verfahren man entscheiden kann, ob aus einem Ausdruck ein anderer Ausdruck folgt. Flir die Pradikatenlogik und deren Teilklassen tritt diese Problemstellung z.B. in der Logik-Programmierung, dem automatischen Be- weisen, in Inferenzkomponenten wissensbasierter Systeme und - aquivalent formuliert - als Erfiillbarkeitsproblem auf. Es hat sich dabei herausgestellt, daB selbst die fiir die Aussagenlogik interes- santen Resultate zu reichhaltig sind, urn sie zusammen mit der Pradikaten- logik in nur einem Zyklus zu behandeln. Da aber viele Ergebnisse fiir eine effiziente Behandlung der vollen Pradikatenlogik von groBem N utzen sind, haben wir uns entschlossen, die Themenbereiche, die von allgemeinem Inter- esse sind, zu sammeln, zusammenhangend aufzuarbeiten und in Buchform zu veroffentlichen. Aber selbst die Beschrankung auf die Aussagenlogik ist nicht ausreichend, urn wirklich aile Problemstellungen und Ansatze aufzu- nehmen. Wir haben daher hier zu Gunsten der Grundlagen und von eher klassischen Inhalten auf Abschnitte iiber z.B. die mehrwertige Aussagenlogik verzichtet.

Die Programmiersprache PROLOG hat in den letzten Jahren, nicht zuletzt durch zahl- reiche Anwendungen im Bereich der Expertensysteme und der natiirlichsprachlichen Ver- arbeitung, immer mehr an Bedeutung gewonnen. Gegeniiber prozeduralen Programmier- sprachen, wie z.B. Pascal, in denen Verfahren zur Losung eines Problems programmiert werden miissen, besteht Programmieren in PROLOG im Prinzip aus einer Beschreibung des Problems. Daraus ergeben sich natiirlich ganz andere Methoden und Schwierigkeiten beim Entwurf eines Prograrnms. Dieses Buch ist aus Vorlesungen an der Universitiit Karlsruhe entstanden. Aus den dabei gemachten Erfahrungen resultiert auch der Aufbau des Buches. Zuerst werden einfache Programme und Konstrukte in Prolog vorgestellt, urn den Leser mit der Vorgehensweise bei der Programmierung in PROLOG vertraut zu machen. N ach einem Exkurs iiber Grundlagen der Logik schliefit sich ein Kapitel iiber die Syntax der Sprache an, wobei wir uns an der Syntax von C-Prolog orientiert haben. Bevor dann eine ausfiihrliche Darstellung der wichtigsten Built-in-Priidikate mit Beispielen stattfindet, wird auf den Ablauf bei der Losungssuche in PROLOG eingegangen. Die Anwendungen sind in zwei Bereiche aufgeteilt. Zum einen werden relativ kurze Bei- spiele iiber Mengen, Parser, Spiele, Logik und Mathematik vorgestellt, und zum anderen ist den Expertensystemen ein ganzes Kapitel gewidmet. Hierbei geht es weniger urn eine Vorstellung und allgemeine Diskussion solcher Systeme, sondern urn die Entwick- lung einer Shell fiir die Implementation von Expertensystemen. 1m Anhang befindet sich dann, bis auf ein Modul fiir die Wissenserfassung, das vollstiindige Programm fiir diese Entwicklungsumgebung.

Die Programmiersprache PROLOG hat in den letzten Jahren, nicht zuletzt durch zahl reiche Anwendungen im Bereich der Expertensysteme und der naturlichsprachlichen Ver arbeitung, immer mehr an Bedeutung gewonnen. Gegenuber prozeduralen Programmier sprachen, wie z.B. Pascal, in denen Verfahren zur Losung eines Problems programmiert werden mussen, besteht Programmieren in PROLOG im Prinzip aus einer Beschreibung des Problems. Daraus ergeben sich naturlich ganz andere Methoden und Schwierigkeiten beim Entwurf eines Programms. Dieses Buch ist aus Vorlesungen an der Universitat Karlsruhe entstanden. Aus den dabei gemachten Erfahrungen resultiert auch der Aufbau des Buches. Zuerst werden einfache Programme und Konstrukte in Prolog vorgestellt, um den Leser mit der Vorgehensweise bei der Programmierung in PROLOG vertraut zu machen. Nach einem Exkurs uber Grundlagen der Logik schliesst sich ein Kapitel uber die Syntax der Sprache an, wobei wir uns an der Syntax von C-Prolog orientiert haben. Bevor dann eine ausfuhrliche Darstellung der wichtigsten Built-in-Pradikate mit Beispielen stattfindet, wird auf den Ablauf bei der Losungssuche in PROLOG eingegangen. Die Anwendungen sind in zwei Bereiche aufgeteilt. Zum einen werden relativ kurze Bei spiele uber Mengen, Parser, Spiele, Logik und Mathematik vorgestellt und zum anderen ist den Expertensystemen ein ganzes Kapitel gewidmet. Hierbei geht es weniger um eine Vorstellung und allgemeine Diskussion solcher Systeme, sondern um die Entwick lung einer Shell fur die Implementation von Expertensystemen. Im Anha.ng befindet sich dann, bis auf ein Modul fur die Wissenserfassung, das vollstandige Programm fur diese Entwicklungsumgebung."