Abstract
Logiweb is an open source, distributed system for publication of machine checked mathematics. It covers all aspects of electronic publishing: high typographical quality, archival, handling of references to previously published results, and publication of refereed volumes. The present paper is itself produced using Logiweb; and the paper is formally correct in the sense that it has been verified by Logiweb. The paper describes the implementation layers of the Logiweb system as seen by the user: the programming layer, the metalogic layer, the tactic layer, and the object proof layer.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Berline, C., Grue, K.: A κ-denotational semantics for Map Theory in ZFC+SI. TCS 179(1–2), 137–202 (1997)
Church, A.: The Calculi of Lambda-Conversion. Princeton University Press, Princeton (1941)
Dobbertin, H., Bosselaers, A., Preneel, B.: RIPEMD-160: A strengthened version of RIPEMD. In: Fast Software Encryption, pp. 71–82 (1996), http://citeseer.nj.nec.com/dobbertin96ripemd.html
Genzen, G.: The Collected Papers of Gerhard Gentzen. In: Szabo, M.E. (ed.) North-Holland (1969)
Grue, K.: Map theory. Theoretical Computer Science 102(1), 1–133 (1992)
Grue, K.: Mathematics and Computation, DIKU, Universitetsparken 1, DK-2100 Copenhagen, 7 edn. vol. 1(3) (2001)
Grue, K.: Map theory with classical maps. Technical Report 02/21, DIKU (2002), http://www.diku.dk/publikationer/tekniske.rapporter/2002/
Grue, K.: Logiweb. In: Kamareddine, F. (ed.) Mathematical Knowledge Management Symposium 2003. Electronic Notes in Theoretical Computer Science, vol. 93, pp. 70–101. Elsevier, New York (2004)
Grue, K.: Logiweb - a system for web publication of mathematics. In: Iglesias, A., Takayama, N. (eds.) ICMS 2006. LNCS, vol. 4151, pp. 343–353. Springer, Heidelberg (2006)
Grue,K.: The layers of logiweb - appendix. Technical report, Logiweb (2007), http://logiweb.eu/logiweb/server/relay/64/BUpCgdix91wGZKohkESIwWkvdwwIhPa08-fhoigBB/2/body/tex/appendix.pdf
Kleene, S.C.: Introduction to Metamathematics. Bibliotheca Mathematica, N-H, vol. 1(1964)
Knuth, D.: The TeXbook. Addison-Wesley, London (1983)
Kohlhase, M.: OMDoc: An open markup format for mathematical documents (version 1.2) (March 16, 2005), http://www.mathweb.org/omdoc/index.html
Mendelson, E.: Introduction to Mathematical Logic, 3rd edn. Wadsworth and Brooks (1987)
Miner, R., Schaeffer, J.: A gentle introduction to MathML (2001), http://www.dessci.com/en/support/tutorials/mathml/default.htm
Muzalewski, M.: An Outline of PC Mizar. Foundation of Logic, Mathematics and Informatics, Mizar User Group, Brussels (1993)
Raggett, D., Batsalle, D.: Adding math to Web pages with EzMath. j-COMP-NET-ISDN 30(1–7), 679–681 (1998)
Skalberg, S.C.: An Interactive Proof System for Map Theory. PhD thesis, University of Copenhagen (October 2002), http://www.mangust.dk/skalberg/phd/
Trybulec, A., Blair, H.: Computer assisted reasoning with MIZAR. In: Joshi, A. (ed.) Proceedings of the 9th International Joint Conference on Artificial Intelligence, Los Angeles, CA, pp. 26–28. Morgan Kaufmann, San Francisco (1985), http://www.mizar.org/
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grue, K. (2007). The Layers of Logiweb. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds) Towards Mechanized Mathematical Assistants. MKM Calculemus 2007 2007. Lecture Notes in Computer Science(), vol 4573. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73086-6_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-73086-6_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73083-5
Online ISBN: 978-3-540-73086-6
eBook Packages: Computer ScienceComputer Science (R0)