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

Gergei Bana, Mitsuhiro Okada

研究成果: Conference contribution

抜粋

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.

元の言語English
ホスト出版物のタイトルComputer Science Logic 2016, CSL 2016
出版者Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
62
ISBN(電子版)9783959770224
DOI
出版物ステータスPublished - 2016 8 1
イベント25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic - Marseille, France
継続期間: 2016 8 292016 9 1

Other

Other25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic
France
Marseille
期間16/8/2916/9/1

    フィンガープリント

ASJC Scopus subject areas

  • Software

これを引用

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