in die operative Logik und Mathematik Zweite Auflage Springer-Verlag Berlin Heidelberg New York 1969 Paul Lorenzen o. Prof. der Philosophie an der Universitat Erlangen Geschaftsfilhrende Herausgeber: Prof. Dr. B. Eckmann Eidgenossische Technische Hochschule Zurich Prof. Dr. B. L. van cler Waerclen Mathematisches Institut der Universitat ZUrich ISBN 978-3-642-86519-0 ISBN 978-3-642-86518-3 (eBook) DOl 10.1007/978-3-642-86518-3 Aile Rechte vorbehalten. Kein Teil dieses Buches darf ohne schriftliche Genehmigung des Springer-Verlages ubersetzt oder in irgendeiner Form vervielfaltigt werden © by Springer-Verlag Berlin· Heidelberg 1955 und 1969 (...) Softcover reprint of the hardcover 2nd edition 1969 Library of Congress Catalog Card Number 73-76724 Titel-Nr. 5061 Vorwort zur zweiten Auflage. Fiir die Neuauflage ist der Text nur unwesentlich geandert worden. Es ist - neben der Korrektur einiger Ungenauigkeiten - vor allem die Terminologie und Symbolik an meine spateren Arbeiten angeglichen. Obwohl ich - verstandlicherweise - jetzt die Ansatze der spateren Arbeiten fiir "sachgemaBer" halte, z. B. eine Logik der Dialoge statt einer Logik der Kalkiile, die Verwendung indefiniter Quantoren statt einer expliziten Konstruktion von Sprachschichten, enthalt diese Neu­ auflage den Inhalt der 1. Auflage unverandert. Der Leser kann also einen Vergleich mit meinen spateren Arbeiten (vgl. Literaturverzeichnis) seIber durchfiihren. Mein Dank gilt wiederum dem Verlag fiir seine entgegenkommende Mitarbeit bei der Vorbereitung dieser Neuauflage. Erlangen, den 1. November I968. PAUL LORENZEN. Vorwort zur ersten Auflage. (shrink)

We investigate logical consequence in temporal logics in terms of logical consecutions. i.e., inference rules. First, we discuss the question: what does it mean for a logical consecution to be 'correct' in a propositional logic. We consider both valid and admissible consecutions in linear temporal logics and discuss the distinction between these two notions. The linear temporal logic LDTL, consisting of all formulas valid in the frame 〈L, ≤, ≥〉 of all integer numbers, is the prime object of our investigation. (...) We describe consecutions admissible LDTL in a semantic way—via consecutions valid in special temporal Kripke/Hintikka models. Then we state that any temporal inference rule has a reduced normal form which is given in terms of uniform formulas of temporal degree 1. Using these facts and enhanced semantic techniques we construct an algorithm, which recognizes consecutions admissible in LDTL. Also, we note that using the same technique it follows that the linear temporal logic L (N) of all natural numbers is also decidable w.r.t. inference rules. So, we prove that both logics LDTL and L (N) are decidable w.r.t. admissible consecutions. In particular, as a consequence, they both are decidable (Known fact), and the given deciding algorithms are explicit. (shrink)

While specifications and verifications of concurrent systems employ Linear Temporal Logic , it is increasingly likely that logical consequence in image will be used in the description of computations and parallel reasoning. Our paper considers logical consequence in the standard image with temporal operations image and image . The prime result is an algorithm recognizing consecutions admissible in image, so we prove that image is decidable w.r.t. admissible inference rules. As a consequence we obtain algorithms verifying the validity of consecutions (...) in image and solving the satisfiability problem. We start by a simple reduction of logical consecutions of image to equivalent ones in the reduced normal form . Then we apply a semantic technique based on image-Kripke structures with formula definable subsets. This yields necessary and sufficient conditions for a consecution to be not admissible in image. These conditions lead to an algorithm which recognizes consecutions admissible in image by verifying the validity of consecutions in special finite Kripke structures of size square polynomial in reduced normal forms of the consecutions. As a consequence, this also solves the satisfiability problem for image. (shrink)

Reasoning About Knowledge is the first book to provide a general discussion of approaches to reasoning about knowledge and its applications to distributed ...