Logical Foundations of Computer Science 无水印原版pdf.pdf

发布时间：2022-06-14 发布人：admin 分类：说明书资料大小：7.08M 资料格式：pdf 举报版权申诉

42db27c4-0d6a-470b-9f6e-08f667f1befd.pdf-第1页.png

第1页 / 共378页

42db27c4-0d6a-470b-9f6e-08f667f1befd.pdf-第2页.png

第2页 / 共378页

42db27c4-0d6a-470b-9f6e-08f667f1befd.pdf-第3页.png

第3页 / 共378页

42db27c4-0d6a-470b-9f6e-08f667f1befd.pdf-第4页.png

第4页 / 共378页

42db27c4-0d6a-470b-9f6e-08f667f1befd.pdf-第5页.png

第5页 / 共378页

42db27c4-0d6a-470b-9f6e-08f667f1befd.pdf-第6页.png

第6页 / 共378页

42db27c4-0d6a-470b-9f6e-08f667f1befd.pdf-第7页.png

第7页 / 共378页

42db27c4-0d6a-470b-9f6e-08f667f1befd.pdf-第8页.png

第8页 / 共378页

Cover

Preface

Organization

Contents

The Completeness Problem for Modal Logic

1 Introduction

2 Background

2.1 Modal Logic

2.2 Bisimulation

2.3 The Complexity of Satisfiability

3 The Completeness Problem and Axiom 5

4 The Completeness Problem and Triviality

4.1 Completeness and K

4.2 Completeness and Consistency

4.3 Completeness, Consistency, and Positive Introspection

4.4 Consistency and Negative Introspection

4.5 Completeness and Modal Logics

5 The Complexity of Completeness

5.1 A Lower Bound

5.2 Upper Bounds

6 Variations and Other Considerations

6.1 Satisfiable and Complete Formulas

6.2 Completeness with Respect to a Model

6.3 Completeness and Normal Forms for Modal Logic

6.4 Completeness up to Depth

6.5 More Logics

References

Justification Awareness Models

1 Context and Motivations

2 Preliminaries

3 Generic Logical Semantics of Justifications

4 Basic Justification Logic J-

4.1 Other Justification Logics

4.2 Sharp Models

5 Justification Awareness

5.1 Justification Awareness Models

5.2 Single-Conclusion Justifications

6 Russell Scenario as a JAM

6.1 Technicalities of the Model

6.2 Can Russell's Scenario Be Made Modal?

7 Kripke Models and Master Justification

8 Discussion

References

A Minimal Computational Theory of a Minimal Computational Universe

1 Introduction

2 Preliminaries

2.1 The Framework

2.2 Computational Theories and Universes

3 Static Extensions by Definitions

4 Real Analysis in J2

4.1 The Natural Numbers

4.2 The Real Line

4.3 Real Functions

5 Conclusion and Further Research

References

A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem

1 Introduction

2 Hilbert's Extended First -Theorem in a Modern Setting

3 A Function Variable Variant of / -Proofs

4 A Sequent-Based Translation into the Function Variable Proof Format

5 A New Version of the Extended First -Theorem

6 Complexity Analysis

7 Conclusion

References

Angluin Learning via Logic

1 Introduction

1.1 What the Algorithm Learns

1.2 Means to Learn

1.3 Related Work

2 Preliminaries

2.1 Coalgebra

2.2 Coalgebraic Modal Logic

2.3 Logical Quotients

3 The Lco Algorithm

3.1 Filtrations and Logical Tables

3.2 Description of the Algorithm

3.3 Termination and Correctness

3.4 Termination Lemmas

4 Examples

5 Conclusions

References

A Universal Algebra for the Variable-Free Fragment of RC

1 Introduction

2 Strictly Positive Logics and Reflection Calculi

2.1 Normal Strictly Positive Logics

2.2 Algebraic Semantics

2.3 The System RC

2.4 The System RC and Fat Normal Forms

3 Ignatiev Frame and Ignatiev RC-Algebra

4 I as the Algebra of Variable-Free RC-Theories

5 A Universal Kripke Frame for RC

References

A Logic of Blockchain Updates

1 Introduction

2 A Simple Blockchain Logic

3 The Deductive System BCL

4 Soundness

5 Normal Form

6 Completeness

7 Conclusion

References

From Display to Labelled Proofs for Tense Logics

1 Introduction

2 Display and Labelled Calculi for Tense Logics

2.1 Display Calculi for Tense Logics

2.2 Labelled Calculi for Tense Logics

3 Interpreting a Display Sequent as a Labelled UT

4 From Labelled UTs to Labelled Sequents

5 Labelled UTs vs Labelled Sequents

References

Notions of Cauchyness and Metastability

1 Almost Cauchyness

2 Metastability

3 Choice Is Necessary

References

A Gödel-Artemov-Style Analysis of Constructible Falsity

1 Introduction

1.1 The Logic of Constructible Falsity

1.2 Artemov's Program of Justification Logic

2 Constructible Falsity and Two Modal Companions

2.1 The Basic System of Constructible Falsity N

2.2 Bi-modal Logics S42 and S42Triv

2.3 Two Faithful Translations of N

3 Two-Agent Logics of Proof and N

3.1 Two-Agent LP with Conversions

3.2 Interpreting N in LP2"3222378 "3222378

4 Preliminary Remarks on Heyting-Brouwer Logic

References

Probabilistic Reasoning About Simply Typed Lambda Terms

1 Introduction

2 Simple Type Assignment

2.1 Lambda Terms and Types

2.2 Lambda Models

3 Probabilistic Logical System for Simply Typed Lambda Terms P

3.1 Syntax of P

3.2 Semantics of P

4 The Axiomatization AxP

5 Completeness

6 Conclusion

References

Polyteam Semantics

1 Introduction

2 From Uni-dependencies to Poly-dependencies

2.1 Dependencies in Team Semantics

2.2 The Notion of Poly-dependence

2.3 A General Notion of a Poly-dependency

2.4 Database Dependencies as Poly-atoms

3 Polyteam Semantics for Complex Formulae

3.1 Syntax and Semantics

3.2 Basic Properties

3.3 Data Exchange in the Polyteam Setting

4 Expressiveness

4.1 Uni-dependencies in Polyteam Semantics

4.2 Poly-dependencies in Polyteam Semantics

5 Conclusion

References

On the Sharpness and the Single-Conclusion Property of Basic Justification Models

1 Introduction

2 Preliminaries

2.1 Basic Justification Models

2.2 Unification

3 Referential Justification Logic Jref

4 Completeness

References

Founded Semantics and Constraint Semantics of Logic Rules

1 Introduction

2 Motivation for Founded Semantics and Constraint Semantics

3 Language

4 Formal Definition of Founded Semantics and Constraint Semantics

5 Properties of Founded Semantics and Constraint Semantics

6 Comparison with Other Semantics

7 Computational Complexity and Extensions

8 Related Work and Conclusion

A Comparison of Semantics for Well-Known Small Examples and More

References

Separating the Fan Theorem and Its Weakenings II

1 Introduction

2 Kripke Structures of Constructive Models

3 FAN Does Not Imply FANc

References

Dialectica Categories for the Lambek Calculus

1 Introduction

2 Related Work

3 The Lambek Calculus

4 Extensions to the Lambek Calculus

5 Categorical Models

5.1 Dialectica Lambek Spaces

6 Type Theory for Lambek Systems

6.1 The Typed Lambek Calculus: L

6.2 The Typed Lambek Calculus: L!

6.3 The Typed Lambek Calculus: L

6.4 The Typed Lambek Calculus: L!

7 Conclusions

References

From Epistemic Paradox to Doxastic Arithmetic

1 Introduction

2 Moore's Paradox

3 The Gödel-Buridan Paradox

4 Moore, Gödel-Buridan, and Dual Moore

5 The Dual Moore

6 The Commissive Moore

7 Doxastic Arithmetic

8 Conclusions

References

A Natural Proof System for Herbrand's Theorem

1 Introduction

2 Expansion Proofs

3 Proof Systems

3.1 Motivation for the Proof Systems

3.2 Open Deduction

3.3 KSh1 and Herbrand Proofs

3.4 KSh2 and Herbrand Normal Form

4 Translations Between KSh2 and Expansion Proofs

4.1 KSh2 to Expansion Proofs

5 Further Work

References

Metastability and Higher-Order Computability

1 Introduction

2 Background and Preliminaries

2.1 Introduction

2.2 The Textbook Example of Metastability

2.3 The Special Fan Functional

2.4 Nonstandard Analysis and Its Computational Content

3 Metastability and Computability

3.1 The Intermediate Value Theorem

3.2 On Maxima, Suprema, and Integrals

3.3 The Principle BD-N

3.4 Computing the Special Fan Functional

References

The Completeness of BCD for an Operational Semantics

1 Introduction

2 Beth Models

References

A Tableau System for Instantial Neighborhood Logic

1 Instantial Neighborhood Logic

2 Tableau System Tinl

3 Termination of Proof-Search in Tinl

4 Soundness of Tinl

5 Completeness of Tinl

6 Conclusions and Discussions

References

Interpretations of Presburger Arithmetic in Itself

1 Introduction

2 Presburger Arithmetic and Definable Sets

3 Interpretations

4 Linear Orders Interpretable in (N,+)

4.1 Functions Definable in Presburger Arithmetic

4.2 Dimension

4.3 Presburger-Definable Linear Orders

5 One-Dimensional Self-interpretations and Visser's Conjecture

6 Multi-dimensional Self-interpretations

References

Author Index

Sergei Artemov Anil Nerode (Eds.) 3 0 7 0 1 S C N L Logical Foundations of Computer Science International Symposium, LFCS 2018 Deerfield Beach, FL, USA, January 8–11, 2018 Proceedings 1 2 3

Lecture Notes in Computer Science 10703 Commenced Publication in 1973 Founding and Former Series Editors: Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen Editorial Board David Hutchison Lancaster University, Lancaster, UK Takeo Kanade Carnegie Mellon University, Pittsburgh, PA, USA Josef Kittler University of Surrey, Guildford, UK Jon M. Kleinberg Cornell University, Ithaca, NY, USA Friedemann Mattern ETH Zurich, Zurich, Switzerland John C. Mitchell Stanford University, Stanford, CA, USA Moni Naor Weizmann Institute of Science, Rehovot, Israel C. Pandu Rangan Indian Institute of Technology, Madras, India Bernhard Steffen TU Dortmund University, Dortmund, Germany Demetri Terzopoulos University of California, Los Angeles, CA, USA Doug Tygar University of California, Berkeley, CA, USA Gerhard Weikum Max Planck Institute for Informatics, Saarbrücken, Germany

More information about this series at http://www.springer.com/series/7407

Sergei Artemov Anil Nerode (Eds.) Logical Foundations of Computer Science International Symposium, LFCS 2018 Deerﬁeld Beach, FL, USA, January 8–11, 2018 Proceedings 123

Editors Sergei Artemov City University of New York New York, NY USA Anil Nerode Cornell University Ithaca, NY USA ISSN 0302-9743 Lecture Notes in Computer Science ISBN 978-3-319-72055-5 https://doi.org/10.1007/978-3-319-72056-2 ISBN 978-3-319-72056-2 (eBook) ISSN 1611-3349 (electronic) Library of Congress Control Number: 2017960856 LNCS Sublibrary: SL1 – Theoretical Computer Science and General Issues © Springer International Publishing AG 2018 This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of the material is concerned, speciﬁcally the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microﬁlms or in any other physical way, and transmission or information storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now known or hereafter developed. The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a speciﬁc statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. The publisher, the authors and the editors are safe to assume that the advice and information in this book are believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors give a warranty, express or implied, with respect to the material contained herein or for any errors or omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in published maps and institutional afﬁliations. Printed on acid-free paper This Springer imprint is published by Springer Nature The registered company is Springer International Publishing AG The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland

Preface The Symposium on Logical Foundations of Computer Science provides a forum for the fast-growing body of work on the logical foundations of computer science, e.g., those areas of fundamental theoretical logic related to computer science. The LFCS series began with “Logic at Botik,” Pereslavl-Zalessky, 1989, which was co-organized by Albert R. Meyer (MIT) and Michael Taitslin (Tver). After that, organization passed to Anil Nerode. Currently LFCS is governed by a Steering Committee consisting of Anil Nerode (General Chair), Stephen Cook, Dirk van Dalen, Yuri Matiyasevich, Gerald Sacks, Andre Scedrov, and Dana Scott. The 2018 Symposium on Logical Foundations of Computer Science (LFCS 2018) took place at the Wyndham Deerﬁeld Beach Resort, Deerﬁeld Beach, Florida, USA, during January 8–11, 2018. This volume contains the extended abstracts of talks selected by the Program Committee for presentation at LFCS 2018. The scope of the symposium is broad and includes constructive mathematics and type theory, homotopy type theory, logic, automata and automatic structures, com- putability and randomness, logical foundations of programming, logical aspects of computational complexity, parameterized complexity, logic programming and con- straints, automated deduction and interactive theorem proving, logical methods in protocol and program veriﬁcation, logical methods in program speciﬁcation and extraction, domain theory logics, logical foundations of database theory, equational logic and term rewriting, logic and topological semantics, linear logic, epistemic and temporal intelligent and multiple-agent system logics, logics of proof and justiﬁcation, non-monotonic rea- soning, logic in game theory and social software, logic of hybrid systems, distributed system logics, mathematical fuzzy logic, system design logics, and other logics in computer science. lambda and combinatory calculi, categorical logics, We thank the authors and reviewers for their contributions. We acknowledge the support of the U.S. National Science Foundation, The Association for Symbolic Logic, Cornell University, the Graduate Center of the City University of New York, and Florida Atlantic University. October 2017 Anil Nerode Sergei Artemov

Organization Steering Committee University of Toronto, Canada Steklov Mathematical Institute, St. Petersburg, Russia Stephen Cook Yuri Matiyasevich Anil Nerode (General Chair) Cornell University, USA Harvard University, USA Gerald Sacks University of Pennsylvania, USA Andre Scedrov Dana Scott Carnegie-Mellon University, USA Utrecht University, The Netherlands Dirk van Dalen Program Committee Sergei Artemov (Chair) Eugene Asarin Steve Awodey Matthias Baaz Lev Beklemishev Andreas Blass Samuel Buss Robert Constable Thierry Coquand Nachum Dershowitz Michael Fellows Melvin Fitting Sergey Goncharov Denis Hirschfeldt Martin Hyland Rosalie Iemhoff Hajime Ishihara Bakhadyr Khoussainov Roman Kuznets Daniel Leivant Robert Lubarsky Victor Marek Lawrence Moss Anil Nerode Hiroakira Ono The City University of New York, USA Université Paris Diderot - Paris 7, France Carnegie Mellon University, USA The Vienna University of Technology, Austria Steklov Mathematical Institute, Moscow, Russia University of Michigan, Ann Arbor, USA University of California, San Diego, USA Cornell University, USA University of Gothenburg, Sweden Tel Aviv University, Israel University of Bergen, Norway The City University of New York, USA Sobolev Institute of Mathematics, Novosibirsk, Russia University of Chicago, USA University of Cambridge, UK Utrecht University, The Netherlands Japan Advanced Institute of Science and Technology, Kanazawa, Japan The University of Auckland, New Zealand The Vienna University of Technology, Austria Indiana University Bloomington, USA Florida Atlantic University, USA University of Kentucky, Lexington, USA Indiana University Bloomington, USA Cornell University, USA Japan Advanced Institute of Science and Technology, Kanazawa, Japan Alessandra Palmigiano Ruy de Queiroz Delft University of Technology, The Netherlands The Federal University of Pernambuco, Recife, Brazil

The Institute of Mathematical Sciences, Chennai, India University of Leeds, UK University of California, San Diego, USA University of Pennsylvania, USA University of Munich, Germany University of Ottawa, Canada University of Ljubljana, Slovenia University of Amsterdam, The Netherlands Radboud University Nijmegen, The Netherlands University of Toronto, Canada VIII Organization Ramaswamy Ramanujam Michael Rathjen Jeffrey Remmel Andre Scedrov Helmut Schwichtenberg Philip Scott Alex Simpson Sonja Smets Sebastiaan Terwijn Alasdair Urquhart Additional Reviewers Josef Berger S. P. Suresh Catalin Dima Giuseppe Greco Yanjing Wang Heinrich Wansing Toshiyasu Arai Lutz Straßburger Rohit Parikh

分享到：

赞收藏

资料库

Logical Foundations of Computer Science 无水印原版pdf.pdf

相关推荐

开发技术

热门标签

最新资料