Search

Edited in collaboration with FoLLI, the Association of Logic, Language and Information this book constitutes the refereed proceedings of the 22nd Workshop on Logic, Language, Information and Computation, WoLLIC 2015, held in the campus of Indiana University, Bloomington, IN, USA in July 2015.The 14 contributed papers, presented together with 8 invited lectures and 4 tutorials, were carefully reviewed and selected from 44 submissions. The focus of the workshop was on interdisciplinary research involving formal logic, computing and programming theory, and natural language and reasoning.

Dieser Katalog weist alle seit 1843 im Springer-Verlag bis zum 30. April 1992 erschienenen Zeitschriften, einschließlich der aus anderen Verlagen übernommenen Titel, nach. Die Titelaufnahmen sind alphabetisch geordnet und beinhalten den Lebenslauf der betreffenden Zeitschrift mit ihren Beziehungen zu anderen Zeitschriften, auch wenn es sich um verlagsfremde Titel handelt, sowie alle Herausgeber mit der Dauer ihrer diesbezüglichen Tätigkeit. Ferner sind die Titel entsprechend dem Jahr ihres Erscheinens und schließlich auch nach Fachgebieten geordnet. Register der Herausgeber und der wissenschaftlichen Vereinigungen, die an der Herausgabe beteiligt waren bzw. sind, beschließen den Band. Der Katalog ergänzt das 1992 anläßlich des 150. Jahrestags der Verlagsgründung erschienene Werk'Der Springer-Verlag. Katalog seiner Veröffentlichungen 1842 - 1945', in dem neben den Büchern auch die bis 1945 erschienen Zeitschriften nachgewiesen sind. Die gesonderte Herausgabe eines Katalogs sämtlicher bis 1992 erschienener Zeitschriften ist in deren zentraler Bedeutung für den Verlag begründet, dessen Rückgrat sie seit über hundert Jahren ideell und materiell darstellen. Sämtliche Bücher und Zeitschriften können auch auf einer CD-ROM recherchiert werden. Wer dieses Medium kennt, weiß, daß der Zugriff einfach und rasch ist sowie viele Verknüpfungsmöglichkeiten zuläßt. Neben den aktuell lieferbaren Titeln enthält die CD-ROM auch alle inzwischen vergriffenen Veröffentlichungen seit dem Jahr der Verlagsgründung. Die CD-ROM-Ausgabe wird in kürzeren Zeitabständen aktualisiert.

This text attempts to change the way we teach logic to beginning students. Instead of teaching logic as a subject in isolation, we regard it as a basic tool and show how to use it. We strive to give students a skill in the propo­ sitional and predicate calculi and then to exercise that skill thoroughly in applications that arise in computer science and discrete mathematics. We are not logicians, but programming methodologists, and this text reflects that perspective. We are among the first generation of scientists who are more interested in using logic than in studying it. With this text, we hope to empower further generations of computer scientists and math­ ematicians to become serious users of logic. Logic is the glue Logic is the glue that binds together methods of reasoning, in all domains. The traditional proof methods -for example, proof by assumption, con­ tradiction, mutual implication, and induction- have their basis in formal logic. Thus, whether proofs are to be presented formally or informally, a study of logic can provide understanding.

On the history of the book: In the early 1990s several new methods and perspectives in au- mated deduction emerged. We just mention the superposition calculus, meta-term inference and schematization, deductive decision procedures, and automated model building. It was this last?eld which brought the authors of this book together. In 1994 they met at the Conference on Automated Deduction (CADE-12) in Nancy and agreed upon the general point of view, that semantics and, in particular, construction of models should play a central role in the?eld of automated deduction. In the following years the deduction groups of the laboratory LEIBNIZ at IMAG Grenoble and the University of Technology in Vienna organized several bilateral projects promoting this topic. This book emerged as a main result of this cooperation. The authors are aware of the fact, that the book does not cover all relevant methods of automated model building (also called model construction or model generation); instead the book focuses on deduction-based symbolic methods for the construction of Herbrand models developed in the last 12 years. Other methods of automated model building, in particular also?nite model building, are mainly treated in the?nal chapter; this chapter is less formal and detailed but gives a broader view on the topic and a comparison of di?erent approaches. Howtoreadthisbook: In the introduction we give an overview of automated deduction in a historical context, taking into account its relationship with the human views on formal and informal proofs.

Computer science departments at universities in the U.S.A. are world renowned. This handy reference guide gives detailed profiles of 40 of the best known among them. The profiles are organized in a uniform layout to present basic information, faculty, curriculum, courses for graduate students, affiilated institutions, facilities, research areas, funding, selected projects, and collaborations. Two full alphabetical listings of professors are included, one giving their universities and the other their research areas. The guide will be indispensible for anyone - student or faculty, not only in the U.S.A. - interested in research and education in computer science in the U.S.A.

Der Autor entwickelt unterhaltsam, gleichzeitig mit mathematischer Strenge, zahlreiche Facetten aus der Wissenschaftsgeschichte, die mit den Anfängen der Informatik in Zusammenhang stehen. Die Beiträge sind über viele Jahre im Informatik Spektrum erschienen und werden nun erstmals in einem Buch zusammengefasst. Die Informatik selbst ist eine junge Wissenschaft, deren Wurzeln tief in die Vergangenheit zurückreichen. Der Autor zeigt dies anhand vieler anregender historischer Notizen.

This Festschrift volume, published in honor of Kurt Mehlhorn on the occasion of his 60th birthday, contains 28 papers written by his former Ph.D. students and colleagues as well as by his former Ph.D. advisor, Bob Constable. The volume's title is a translation of the title of Kurt Mehlhorn's first book,'Effiziente Algorithmen', published by Teubner-Verlag in 1977. This Festschrift demonstrates how the field of algorithmics has developed and matured in the decades since then. The papers included in this volume are organized in topical sections on models of computation and complexity; sorting and searching; combinatorial optimization with applications; computational geometry and geometric graphs; and algorithm engineering, exactness and robustness.

For the past 25 years the CADE conference has been the major forum for the presentation of new results in automated deduction. This volume contains the papers and system descriptions selected for the 17th International Conference on Automated Deduction, CADE-17, held June 17-20, 2000,at Carnegie Mellon University, Pittsburgh, Pennsylvania (USA). Fifty-three research papers and twenty system descriptions were submitted by researchers from?fteen countries. Each submission was reviewed by at least three reviewers. Twenty-four research papers and?fteen system descriptions were accepted. The accepted papers cover a variety of topics related to t- orem proving and its applications such as proof carrying code, cryptographic protocol veri?cation, model checking, cooperating decision procedures, program veri?cation, and resolution theorem proving. The program also included three invited lectures: “High-level veri?cation using theorem proving and formalized mathematics” by John Harrison, “Sc- able Knowledge Representation and Reasoning Systems” by Henry Kautz, and “Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice” by Carl Seger. Abstracts or full papers of these talks are included in this volume.In addition to the accepted papers, system descriptions, andinvited talks, this volumecontains one page summaries of four tutorials and?ve workshops held in conjunction with CADE-17.

This volume constitutes the proceedings of the16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003) held September 8–12, 2003 in Rome, Italy. TPHOLs covers all aspects of theorem proving in higher order logics as well as related topics in theorem proving and veri?cation. TPHOLs 2003 was co-located with TABLEAUX, the International Con- rence on Automated Reasoning with Analytic Tableaux and Related Methods, and with Calculemus, the Symposium on the Integration of Symbolic Compu- tion and Mechanized Reasoning. There were 50 papers submitted to TPHOLs in the full research category, each of which was refereed by at least 3 reviewers, selected by the program c- mittee.Ofthesesubmissions,21wereacceptedforpresentationattheconference and publication in this volume. In keeping with tradition, TPHOLs 2003 also o?ered a venue for the presentation of work in progress, where researchers - vite discussion by means of a brief preliminary talk and then discuss their work at a poster session. A supplementary proceedings containing associated papers for work in progress was published by the computer science department at the Universit¨ at Freiburg. The organizers are grateful to Jean-Raymond Abrial, Patrick Lincoln, and Dale Miller for agreeing to give invited talks at TPHOLs 2003. The TPHOLs conference traditionally changes continent each year in order to maximize the chances that researchers from around the world can attend.