Abstract
ΩMEGA [7], a mathematical assistant environment comprising an interactive proof assistant, a proof planner, a structured knowledge base, a graphical user interface, access to external reasoners, etc., is being developed since the early 90’s at Saarland University. Similar to HOL4, Isabelle/HOL, Coq, or Mizar, the overall goal of the project is to develop a system platform for formal methods (not only) in mathematics and computer science. In ΩMEGA, user and system interact in order to produce verifiable and trusted proofs. By continously improving (not only) automation and interaction support in the system we want to ease the usually very tedious formalization and proving task for the user.
Funded by the DFG SFB378 (Project OMEGA) and by EPSRC under grant EP/D070511/1.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Autexier, S.: The core calculus. In: Nieuwenhuis, R. (ed.) Automated Deduction – CADE-20. LNCS (LNAI), vol. 3632, Springer, Heidelberg (2005)
Benzmüller, C., Vo, Q.B.: Mathematical domain reasoning tasks in natural language tutorial dialog on proofs. In: Proc. AAAI-05, AAAI Press/The MIT Press (2005)
Benzmüller, C., et al.: Natural language dialog with a tutor system for mathematical proofs. In: Ullrich, C., Siekmann, J.H., Lu, R. (eds.) Cognitive Systems. LNCS (LNAI), vol. 4429, Springer, Heidelberg (2007)
Benzmüller, C., et al.: Diawoz-II - a tool for wizard-of-oz experiments in mathematics. In: Freksa, C., Kohlhase, M., Schill, K. (eds.) KI 2006. LNCS (LNAI), vol. 4314, Springer, Heidelberg (2007)
Benzmüller, C., et al.: Proof planning: A fresh start? In: Proc. of IJCAR 2001 Workshop: Future Directions in Automated Reasoning, Siena, Italy (2001)
Dietrich, D., Buckley, M.: Verification of Proof Steps for Tutoring Mathematical Proofs. In: Proc. AIED 2007 (to appear)
Siekmann, J., et al.: Computer supported mathematics with omega. J. Applied Logic 4(4), 533–559 (2006)
Autexier, S., Dietrich, D.: Synthesizing Proof Planning Methods and Oants Agents from Mathematical Knowledge. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol. 4108, Springer, Heidelberg (2006)
McMath, D., Rozenfeld, M., Sommer, R.: A computer environment for writing ordinary mathematical proofs. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 507–516. Springer, Heidelberg (2001)
Zinn, C.: A computational framework for understanding mathematical discourse. Logic J. of the IGPL 11, 457–484 (2003)
Dietrich, D.: The tasklayer of the omega system. Master’s thesis, Universität des Saarlandes, Saarbrücken, Germany (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Benzmüller, C., Dietrich, D., Schiller, M., Autexier, S. (2007). Deep Inference for Automated Proof Tutoring?. In: Hertzberg, J., Beetz, M., Englert, R. (eds) KI 2007: Advances in Artificial Intelligence. KI 2007. Lecture Notes in Computer Science(), vol 4667. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74565-5_34
Download citation
DOI: https://doi.org/10.1007/978-3-540-74565-5_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74564-8
Online ISBN: 978-3-540-74565-5
eBook Packages: Computer ScienceComputer Science (R0)