×

Project abstract: logic atlas and integrator (LATIN). (English) Zbl 1278.68285

Davenport, James H. (ed.) et al., Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22672-4/pbk). Lecture Notes in Computer Science 6824. Lecture Notes in Artificial Intelligence, 289-291 (2011).
Summary: LATIN aims at developing methods, techniques, and tools for interfacing logics and related formal systems. These systems are at the core of mathematics and computer science and are implemented in systems like (semi-)automated theorem provers, model checkers, computer algebra systems, constraint solvers, or concept classifiers. Unfortunately, these systems have differing domains of applications, foundational assumptions, and input languages, which makes them non-interoperable and difficult to compare and evaluate in practice.
For the entire collection see [Zbl 1218.68014].

MSC:

68T27 Logic in artificial intelligence
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T., Rabe, F., Sojakova, K.: Towards Logical Frameworks in the Heterogeneous Tool Set Hets. In: Workshop on Abstract Development Techniques. LNCS. Springer, Heidelberg (to appear, 2011) · Zbl 1278.68286
[2] Gičeva, J., Lange, C., Rabe, F.: Integrating Web Services into Active Mathematical Documents. In: Carette, J., Dixon, L., Sacerdoti Coen, C., Watt, S. (eds.) MKM 2009, Held as Part of CICM 2009. LNCS, vol. 5625, pp. 279–293. Springer, Heidelberg (2009) · Zbl 1247.68314 · doi:10.1007/978-3-642-02614-0_24
[3] Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39(1), 95–146 (1992) · Zbl 0799.68134 · doi:10.1145/147508.147524
[4] Horozal, F., Rabe, F.: Representing Model Theory in a Type-Theoretical Logical Framework. Theoretical Computer Science (to appear, 2011), http://kwarc.info/frabe/Research/HR_folsound_10.pdf · Zbl 1236.03027 · doi:10.1016/j.tcs.2011.03.022
[5] Iancu, M., Rabe, F.: Formalizing Foundations of Mathematics. Mathematical Structures in Computer Science (to appear, 2011), http://kwarc.info/frabe/Research/IR_foundations_10.pdf · Zbl 1242.03031 · doi:10.1017/S0960129511000144
[6] Kohlhase, M., Rabe, F., Zholudev, V.: Towards MKM in the Large: Modular Representation and Scalable Software Architecture. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P., Rideau, L., Rioboo, R., Sexton, A. (eds.) AISC 2010. LNCS, vol. 6167, pp. 370–384. Springer, Heidelberg (2010) · Zbl 1278.68297 · doi:10.1007/978-3-642-14128-7_32
[7] Mossakowski, T., Maeder, C., Lüttich, K.: The Heterogeneous Tool Set. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007) · Zbl 05185799 · doi:10.1007/978-3-540-71209-1_40
[8] Pfenning, F., Schürmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999) · doi:10.1007/3-540-48660-7_14
[9] Rabe, F.: A Logical Framework Combining Model and Proof Theory. Submitted to Mathematical Structures in Computer Science (2010), http://kwarc.info/frabe/Research/rabe_combining_09.pdf · Zbl 1326.03082
[10] Rabe, F.: Representing Isabelle in LF. In: Crary, K., Miculan, M. (eds.) Logical Frameworks and Meta-Languages: Theory and Practice. EPTCS, vol. 34, pp. 85–100 (2010) · doi:10.4204/EPTCS.34.8
[11] Rabe, F., Kohlhase, M.: A Scalable Module System. Under review (2011), http://arxiv.org/abs/1105.0548 · Zbl 1358.68283
[12] Rabe, F., Schürmann, C.: A Practical Module System for LF. In: Cheney, J., Felty, A. (eds.) Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), pp. 40–48. ACM Press, New York (2009)
[13] Zholudev, V., Kohlhase, M.: TNTBase: a Versioned Storage for XML. In: Proceedings of Balisage: The Markup Conference 2009. Balisage Series on Markup Technologies, vol. 3. Mulberry Technologies, Inc., (2009)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.