TY - GEN
T1 - Semantics for "enough-certainty" and fitting's embedding of classical logic in S4
AU - Bana, Gergei
AU - Okada, Mitsuhiro
N1 - Publisher Copyright:
© Gergei Bana and Mitsuhiro Okada licensed under Creative Commons License CC-BY.
PY - 2016/8/1
Y1 - 2016/8/1
N2 - 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.
AB - 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.
KW - Asymptotic probabilities
KW - First-order logic
KW - Fitting embedding
KW - Possible-world semantics
KW - Verification of complexity-theoretic properties
UR - http://www.scopus.com/inward/record.url?scp=85012865578&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85012865578&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CSL.2016.34
DO - 10.4230/LIPIcs.CSL.2016.34
M3 - Conference contribution
AN - SCOPUS:85012865578
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - Computer Science Logic 2016, CSL 2016
A2 - Talbot, Jean-Marc
A2 - Regnier, Laurent
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic
Y2 - 29 August 2016 through 1 September 2016
ER -