Automated Human-Like Reasoning with Theorema 2.0

Description

Theorema is a system aimed at the support of mathematical theory exploration. The core activities in theory exploration are defining new mathematical concepts and proving their properties. The main focus of Theorema is on human-like style in both input and output. This means that mathematical input should appear as though written in a good math textbook, and proofs generated by the system should read as written by a smart student. Theorema uses programmable expression syntax in Mathematica to define its own version of a mathematical language based on sets, tuples and common constructs of predicate logic. Customized cascading stylesheets allow one to compose entire theories in notebooks with enhanced functionality and appealing style. The reasoning engine is based on a deduction calculus in natural style making heavy use of syntactic and semantic pattern matching as available in Mathematica for decades. Theorema is developed as a standard Mathematica add-on package and is available free of charge under a GNU GPL license. The applications of the Theorema system reach from higher-level education to research mathematics. The more computational thinking brings algorithms into the classrooms, the more will correctness of algorithms become one of the key topics for future generations of students. Formal trusted proving will be the enabling technique in this area—but also for pure mathematics, the significance of formal reasoning will increase. The Theorema system has recently been used for a formalization of second-price auctions in theoretical economics.

Period	15 Jun 2018
Event title	European Wolfram Technology Conference (EWTC'2018)
Event type	Conference
Location	United KingdomShow on map