Document Open Access Logo

Semantics for "Enough-Certainty" and Fitting's Embedding of Classical Logic in S4

Authors Gergei Bana, Mitsuhiro Okada

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2016.34.pdf
  • Filesize: 483 kB
  • 17 pages

Document Identifiers

Subject Classification

Keywords
  • first-order logic
  • possible-world semantics
  • Fitting embedding
  • asymptotic probabilities
  • verification of complexity-theoretic properties

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Gergei Bana and Mitsuhiro Okada. Semantics for "Enough-Certainty" and Fitting's Embedding of Classical Logic in S4. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CSL.2016.34

Author Details

Gergei Bana
Mitsuhiro Okada

References

  1. G. Bana, P. Adão, and H. Sakurada. Computationally Comlete Symbolic Attacker in Action. In Proceedings of the 32nd International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'12), LIPIcs, pages 546-560. Schloss Dagstuhl, 2012. Google Scholar
  2. G. Bana and H. Comon-Lundh. Towards unconditional soundness: Computationally complete symbolic attacker. Available at IACR ePrint Archive, Report 2012/019. Google Scholar
  3. G. Bana and H. Comon-Lundh. Towards unconditional soundness: Computationally complete symbolic attacker. In Proceedings of the 1st International Conference on Principals of Security and Trust (POST'12), LNCS, pages 189-208. Springer, 2012. Google Scholar
  4. G. Bana, K. Hasebe, and M. Okada. Computationally complete symbolic attacker and key exchange. In Proceedings of the 20th ACM SIGSAC Conference on Computer and Communications Security (CCS'13), pages 1231-1246. ACM, 2013. Google Scholar
  5. P. J. Cohen. Set theory and the continuum hypothis. W. A. Benjamin, Inc., New York, 1966. Google Scholar
  6. A. Datta, A. Derek, J. C. Mitchell, and B. Warinschi. Computationally sound compositional logic for key exchange protocols. In Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW'06), pages 321-334. IEEE, 2006. Google Scholar
  7. M. Fitting. An embedding of classical logic in s4. The Journal of Symbolic Logic, 35(4):529-534, 1970. Google Scholar
  8. N. Friedman, J. Y. Halpern, and D. Koller. First-order conditional logic for default reasoning revisited. ACM Transactions on Computational Logic, 1(2):175-207, 2000. Google Scholar
  9. K. Gödel. Eine interpretation des intuitionistischen aussagenkalküls. Ergebnisse eines Mathematischen Kolloquiums, 4:39-40, 1933. Google Scholar
  10. K. Gödel. Zur intuitionistischen arithmetik und zahlentheorie. Ergebnisse eines Mathematischen Kolloquiums, 4:34-38, 1933. Google Scholar
  11. M. Goldszmidt, P. Morris, and J. Pearl. A maximum entropy approach to nonmonotonic reasoning. IEEE Transactions on Pattern Analysis and Machine Intelligence, 15(3):220-232, March 1993. Google Scholar
  12. A. N. Kolmogorov. O principe tertium non datur (russian). Matematiceskij Sbornik, 32:646-667, 1925. Google Scholar
  13. H. Rasiowa and R. Sikorski. The Mathematics of Metamathematics. Polish Scientific Publishers, 1963. Google Scholar
  14. D. Scott and R. Solovay. Boolean-valued models of set theory. unpublished and circulated, 1967. Google Scholar
  15. R. M. Smullyan and M. Fitting. Set Theory and the Continuum Problem. Oxford University Press, 1996. revised addition by Dover, 2006. Google Scholar
  16. J. Väänänen. Dependence Logic: A New Approach to Independence Friendly Logic. Cambridge University Press, 2007. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact