Simulation Logic

• Authors: Allwein Gerard , Harrison William L. , Andrews David
• Languages of publication: EN

Abstracts

EN

Simulation relations have been discovered in many areas: Computer Science, philosophical and modal logic, and set theory. However, the simulation condition is strictly a first-order logic statement. We extend modal logic with modalities and axioms, the latter’s modeling conditions are the simulation conditions. The modalities are normal, i.e., commute with either conjunctions or disjunctions and preserve either Truth or Falsity (respectively). The simulations are considered arrows in a category where the objects are descriptive, general frames. One can augment the simulation modalities by axioms for requiring the underlying modeling simulations to be bisimulations or to be p-morphisms. The modal systems presented are multi-sorted and both sound and complete with respect to their algebraic and Kripke semantics.

Keywords

EN

modal logic; simulations; Hilbert systems; Kripke; modal algebras

• Publisher: Uniwersytet Mikołaja Kopernika (Nicolaus Copernicus University in Toruń)
• Journal: Logic and Logical Philosophy
• Year: 2014
• Volume: 23
• Issue: 3
• Pages: 277–299

Dates

published

2014-09-01

online

2013-09-15

Contributors

author

Allwein Gerard

• Naval Research Laboratory, Code 5543, Washington, DC 20375, U.S.A.

author

Harrison William L.

• Dept. of Computer Science, University of Missouri, Columbia, Missouri, U.S.A.

author

Andrews David

• Dept. of Computer Science and Computer Engineering, University of Arkansas, Fayetteville, Arkansas 72701

References

• Adamek, J., and J. Rosicky, Locally Presentable and Accessible Categories, London Mathematical Society, 1994. Lecture Note Series 189.
• Gerard Allwein, G., and J.M. Dunn, “Kripke models for linear logic”, Journal of Symbolic Logic, 58 (1993): 514–545. DOI: 10.2307/2275217
• Allwein, G., and W.L. Harrison, “Partially ordered modalities”, pages 1–20 in Proceedings of the Advances in Modal Logic Conference, 2010, Springer-Verlag, 2010.
• Birkhoff, G., and J.D. Lipson, “Heterogeneous algebras”, Journal of Computational Theory, 8 (1968): 115–133. DOI: 10.1016/S0021-9800(70)80014-X
• Blackburn, P., M. de Rijke, and Y. Venema, Modal Logic, Cambridge University Press, 2001. Cambridge Tracts in Theoretical Computer Science, No. 53.
• Chellas, B.F., Modal Logic: An Introduction, Cambridge University Press, 1980.
• Chou, Ching-Tsun, “A simple treatment of property preservation via simulation”, Technical Report, Department of Computer Science, University of California at Los Angeles, 1995.
• Dummett, M.A.E., and E.J. Lemmon, “Modal logics between S4 and S5”, Zeitschrift für mathematische Logik and Grundlagen der Mathematik, 5 (1959): 250–264.
• Dunn, J.M., “Gaggle theory: An abstraction of galois connections and residuation with applications to negation and various logical operations”, pages 31–51 in Logics in AI, Proceedings European Workshop JELIA, LNCS 478, Springer-Verlag, 1990.
• Dunn, J.M., and G. Hardegree, Algebraic Methods in Philosophical Logic, Oxford Logic Guides 41. Oxford University Press, 2001.
• Freyd, P.J., and A. Scedrov, Categories and Allegories, North-Holland, 1990.
• Kupke, C., A. Kurz, and Y. Venema, “Stone coalgebras”, pages 170–190 in Coalgebraic Methods in Computer Science, Electronic Notes in Theoretical Computer Science, H.P. Gumm (ed.), volume 82 of 1, 2003.
• Lemmon, E.J., “An Introduction to Modal Logic: The “Lemmon Notes””, American Philosophical Quarterly Monograph Series, 11, 1977.
• Meyer, R.K., “New axiomatics for relevant logics. I”, Journal of Philosophical Logic, 3 (1974): 53–86. DOI: 10.1007/BF00652071
• Sangiorgi, D., “On the origins of bisimulation and coinduction”, ACM Trans. Program. Lang. Syst., 31 (2009), 4:15:1–15:41. DOI: 10.1145/1516507.1516510
• Sangiorgi, D.. Introduction to Bisimulation and Coinduction, Cambridge University Press, 2012.
• Szor, P., The Art of Computer Virus Research and Defense, AddisonWesley Professional, 2005.
• Wells, Ch., and M. Barr, “The formal description of data types using sketches”, pages 490–527 in LNCS 298, Mathematical Foundations of Programming Language Semantics, 1987.

Identifiers

DOI

10.12775/LLP.2013.027