2026-07-21T19:24:35Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6574 2024-03-06T10:38:45Z ddc:004 open_access

Semantics for "Enough-Certainty" and Fitting's Embedding of Classical Logic in S4 Bana, Gergei Okada, Mitsuhiro first-order logic possible-world semantics Fitting embedding asymptotic probabilities verification of complexity-theoretic properties 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Gergei Bana and Mitsuhiro Okada 2016 Is Part Of LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2016.34 urn:nbn:de:0030-drops-65746 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.34 eng https://creativecommons.org/licenses/by/3.0/legalcode