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
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Volume62
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

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

    Fingerprint

Keywords

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

ASJC Scopus subject areas

  • Software

Cite this

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