Matematisk logik

Oiva Ketonen (1913--2000) was the closest to a student the creator of modern proof theory Gerhard Gentzen ever had. Their encounter took place in 1938--39 in Göttingen, with Ketonen hoping to receive a suitable topic for a doctoral dissertation and Gentzen instead deeply immersed in attempts at proving the consistency of analysis. Ketonen's thesis of 1944, his only work in logic, introduced what is today called the G3-sequent calculus. It is his best-known discovery, a sequent calculus for classical propositional logic the logical rules of which are all invertible. Few read his thesis, the results of which were instead made available through a long review by Paul Bernays. Ketonen's calculus is the basis of Evert Beth's tableau method and of the sequent calculi in Stephen Kleene's influential {\it Introduction to Metamathematics}. A second result was a sharpening of the midsequent theorem, by which the number of quantifier inferences with eigenvariables could be minimized. The existence of a weakest possible midsequent followed, in the sense that if any midsequent is derivable, a weakest one is. Turning this into a contrapositive, Ketonen found a purely syntactic method for proofs of underivability that he applied to affine plane geometry. His result, in modern terms, was a positive solution to the word problem for the universal fragment of plane affine geometry, with a syntactic proof of underivability of the parallel postulate from the rest of the affine axioms as a corollary.

The idea of a knowledge base lies at the heart of symbolic or "good old-fashioned" artificial intelligence (GOFAI). A knowledge-based systemdecides how to act by running formal reasoning procedures over a body of explicitly represented knowledge, its knowledge base. The system isnot programmed for specific tasks; rather, it is told what it needs to know, and expected to infer the rest.This book is about the logic of such knowledge bases. It describes in detail the relationship between symbolic representations of knowledge and abstract states of knowledge, exploring along the way, the foundations of knowledge, knowledge bases, knowledge-based systems, and knowledge representation and reasoning. Assuming some familiarity with first-order predicate logic, the book offers a rigorous mathematical model of knowledge that is general and expressive, yet more workable in practice than previous models.The first edition of the book appeared in the year 2000, and since then its model of knowledge has been applied and extended in a number of ways.This second edition incorporates a number of new results about the logic of knowledge bases, including default reasoning, reasoning about actionand change, and tractable reasoning.Hector Levesque is Professor Emeritus in the Department of Computer Science, University of Toronto. Gerhard Lakemeyer is Professor and Chair of the Department of Computer Science, RWTH Aachen University, and Professor (status only) in the Department of Computer Science, University of Toronto.

This Festschrift is in honour of Professor Marie Düí, V¿B - Technical University of Ostrava. The 16 contributions, authored by 24 colleagues, runthe gamut from foundations in logic and theoretical computer science through philosophical logic, multi-agent systems and theory of communicationto personal recollections. Marie Düí is best known for her profound and extensive work on both the foundations and multiple applications of Transparent Intensional Logic, originally developed by Pavel Tichý in the late 1960s. Her work, whether single-authored or co-authored, has appeared in various high-level journals. In 2008 the Rector of her home university granted Marie the award Outstanding Results in the Development of Science and Research.The 2010 monograph Procedural Semantics for Hyperintensional Logic earned Marie and her coauthors the prestigious Award for OutstandingResults of Major Scientific Importance from the Academy of Sciences of the Czech Republic. The major achievements of Transparent IntensionalLogic that Marie has been involved in over the last decade have been compiled into the volume Transparent Intensional Logic: Selected RecentEssays, also published by College Publications.

This book constitutes the proceedings of the 25th International Symposium on Practical Aspects of Declarative Languages, PADL 2023, which was held in Boston, MA, USA, in January 2023.The 15 full papers and 4 short papers presented in this volume were carefully reviewed and selected from 36 submissions. The papers are organized in the following topical sections: Functional Programming; Logic Programming.

Model Validation and Uncertainty Quantification, Volume 3:  Proceedings of the 39th IMAC, A Conference and Exposition on Structural Dynamics, 2021, the third volume of nine from the Conference brings together contributions to this important area of research and engineering.  The collection presents early findings and case studies on fundamental and applied aspects of Model Validation and Uncertainty Quantification, including papers on:Inverse Problems and Uncertainty QuantificationControlling UncertaintyValidation of Models for Operating EnvironmentsModel Validation & Uncertainty Quantification: Decision MakingUncertainty Quantification in Structural DynamicsUncertainty in Early Stage DesignComputational and Uncertainty Quantification Tools

This book introduces the notion of an effective Kan fibration, a new mathematical structure which can be used to study simplicial homotopy theory. The main motivation is to make simplicial homotopy theory suitable for homotopy type theory. Effective Kan fibrations are maps of simplicial sets equipped with a structured collection of chosen lifts that satisfy certain non-trivial properties. Here it is revealed that fundamental properties of ordinary Kan fibrations can be extended to explicit constructions on effective Kan fibrations. In particular, a constructive (explicit) proof is given that effective Kan fibrations are stable under push forward, or fibred exponentials. Further, it is shown that effective Kan fibrations are local, or completely determined by their fibres above representables, and the maps which can be equipped with the structure of an effective Kan fibration are precisely the ordinary Kan fibrations. Hence implicitly, both notions still describe the same homotopy theory. These new results solve an open problem in homotopy type theory and provide the first step toward giving a constructive account of Voevodsky's model of univalent type theory in simplicial sets.

The aim of this book is to draw a holistic picture of ongoing online teaching-activities before and during the lockdown period and present the meaning and future of e-learning from students' points of view, taking into consideration their attitudes and expectations as well as industry 4.0 and society 5.0 aspects.

This book presents the mathematics of quantum computation. The purpose is to introduce the topic of quantum computing to students in computer science, physics and mathematics who have no prior knowledge of this field.

This primer on mathematics formalisation provides a rapid, hands-on introduction to proof verification in Lean.After a quick introduction to Lean, the basic techniques of human-readable formalisation are introduced, illustrated by simple examples on maps, induction and real numbers. Subsequently, typical design options are discussed and brought to life through worked examples in the setting of simplicial complexes (a higher-dimensional generalisation of graph theory). Finally, the book demonstrates how current research in algebraic and geometric topology can be formalised by means of suitable abstraction layers.Informed by the author's recent teaching and research experience, this book allows students and researchers to quickly get started with formalising and checking their proofs. The core material of the book is accessible to mathematics students with basic programming skills. For the final chapter, familiarity with elementary category theory and algebraic topology is recommended.

Die Schulmathematik vermittelt meist nur einen sehr eingeschränkten Einblick in die beweisorientierte und axiomatisch aufgebaute moderne Mathematik ¿ Studienanfänger werden daher oft unvorbereitet von der Hochschulmathematik getroffen.Dieses Lehrbuch erleichtert den nötigen Übergang zum selbstständigen Erarbeiten und Lernen mathematischer Beweise und Inhalte: Es motiviert die Lesenden, selbst aktiv zu werden und sich alleine an den gegebenen Problemstellungen zu versuchen. Dabei wird viel Wert auf leichte Sprache, ausführliche Erklärungen und detaillierte Beispiele gelegt. Somit ist das Buch optimal zum Selbststudium, als Material für Online-Lehrveranstaltungen oder als Ergänzung zu klassischen Mathematik-Vorkursen geeignet.Die einzelnen Kapitel können weitgehend eigenständig und selektiv gelesen bzw. bearbeitet werden, sind aber einheitlich aufgebaut: Jedes Kapitel orientiert sich inhaltlich an einer zu Beginn dargestellten Leitfrage. Auf dem Weg zur Antwort werden die Lesenden von ausführlichen Erläuterungen, Schnellaufgaben, klassischen Übungsaufgaben und Wiederholungsaufgaben begleitet. Die Relevanz der Ergebnisse wird abschließend erläutert; an einigen Stellen gehen die Autoren sogar auf aktuelle Forschung ein oder geben Ausblicke auf tiefere mathematische Erkenntnisse.Die mathematische Basis dieses Buchs ist die zweisemestrige Vorlesung zur Elementarmathematik für das Haupt- und Realschul-Lehramt an der Goethe Universität Frankfurt. Daher eignet sich das Buch besonders gut für Lehramtsstudierende (auch für das gymnasiale Lehramt), als Anregung für Lehrkräfte oder als Ausblick für motivierte Schüler sowie als Brückenkursmaterial.

Starting with the historical evolution of computer and communications networks and their security, the book then arrives at the main definitions of cryptography and network security. Next, the basics of information theory, how to measure information, the information associated with a certain source are also discussed. Source codes are presented, along with the concepts of information transmission, joint information, conditional entropy, mutual information and channel capacity. Computer networks are discussed, including the main protocols and network architectures, and the important TCP/IP protocol. Network security, a topic intrinsically connected to computer networks and the Internet, is presented, along with information about basic hacker attacks, alternatives to prevent attacks, data protection and secure protocols. The information theoretical aspects of cryptography are described including the hash function. An appendix includes a review of probability theory. Illustrations and graphics will help the reader understand the theory.

During his lifetime, Kurt Godel was not well known outside the professional world of mathematicians, philosophers and theoretical physicists. Early in his career, for his doctoral thesis and then for his Habilitation (Dr.Sci.), he wrote earthshaking articles on the completeness and provability of mathematical-logical systems, upsetting the hypotheses of the most famous mathematicians/philosophers of the time. He later delved into theoretical physics, finding a unique solution to Einstein's equations for gravity, the 'Godel Universe', and made contributions to philosophy, the guiding theme of his life. This book includes more details about the context of Gdel's life than are found in earlier biographies, while avoiding an elaborate treatment of his mathematical/scientific/philosophical works, which have been described in great detail in other books. In this way, it makes him and his times more accessible to general readers, and will allow them to appreciate the lasting effects of Gdel's contributions (the latter in a more up-to-date context than in previous biographies, many of which were written 15-25 years ago). His work spans or is relevant to a wide spectrum of intellectual endeavor, and this is emphasized in the book, with recent examples. This biography also examines possible sources of his unusual personality, which combined mathematical genius with an almost childlike naivet concerning everyday life, and striking scientific innovations with timidity and hesitancy in practical matters. How he nevertheless had a long and successful career, inspiring many younger scholars along the way, with the help of his loyal wife Adele and some of his friends, is a fascinating story in human nature.