Semantics for "enough-certainty" and fitting's embedding of classical logic in S4

Gergei Bana, Mitsuhiro Okada

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

In this work we look at how Fitting's embedding of first-order classical logic into first-order S4 can help in reasoning when we are interested in satisfaction "in most cases", when first-order properties are allowed to fail in cases that are considered insignificant. We extend classical semantics by combining a Kripke-style model construction of "significant" events as possible worlds with the forcing-Fitting-style semantics construction by embedding classical logic into S4. We provide various examples. Our main running example is an application to symbolic security protocol verification with complexity-theoretic guarantees. In particular, we show how Fitting's embedding emerges entirely naturally when verifying trace properties in computer security.

Original languageEnglish
Title of host publicationComputer Science Logic 2016, CSL 2016
EditorsJean-Marc Talbot, Laurent Regnier
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959770224
DOIs
Publication statusPublished - 2016 Aug 1
Event25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic - Marseille, France
Duration: 2016 Aug 292016 Sep 1

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume62
ISSN (Print)1868-8969

Other

Other25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic
CountryFrance
CityMarseille
Period16/8/2916/9/1

Keywords

  • Asymptotic probabilities
  • First-order logic
  • Fitting embedding
  • Possible-world semantics
  • Verification of complexity-theoretic properties

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Semantics for "enough-certainty" and fitting's embedding of classical logic in S4'. Together they form a unique fingerprint.

  • Cite this

    Bana, G., & Okada, M. (2016). Semantics for "enough-certainty" and fitting's embedding of classical logic in S4. In J-M. Talbot, & L. Regnier (Eds.), Computer Science Logic 2016, CSL 2016 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 62). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2016.34