Theorema 2.0: An Open-Source Mathematical Assistant System for Automated and Interactive Reasoning

Description

Theorema 2.0 stands for a re-design including a complete re-implementation of the Theorema system, which was originally designed, developed, and implemented by Bruno Buchberger and his Theorema group at RISC. In this talk, we want to present the current status of the implementation and highlight the system's capabilities in the direction of program verification. Automated theorem proving is of course an integral part of program verification. So every automated theorem proving system has its obvious application in program verification. The Theorema system may be a particularly well-suited platform for program verification for two reasons: \begin{enumerate} \item Programs and their properties are formulated in the same language, hence reasoning and execution of algorithms can be done within one system without any translation requirements between different systems and formalisms. \item Theorema 2.0 also offers language constructs for imperative (procedural) programming, which can be executed based on corresponding constructs in the Mathematica programming language. In this way, programs become objects in the Theorema language, what can be manipulated in various ways, e.g. for the generation of verification conditions. \end{enumerate} On the level of proving, Theorema 2.0 offers fully automated and interactive proving in an integrated environment. The user may choose between different levels of interactivity. Both the proof search and the behavior of individual inference rules may be influenced through user interaction. In any case, the result is always a proof in natural language similar to a textbook proof. Moreover, the level of detail shown in the proof is configurable by the user. Theorema 2.0 is based on Mathematica and runs on all platforms, on which Mathematica is available. It is open source licensed under GPL and is (will be) available at GitHub.

Period	24 Oct 2013
Event title	PAS'2013: Second International Seminar on Program Verification, Automated Debugging and Symbolic Computation
Event type	Conference
Location	ChinaShow on map