Theorema 2.0: A First Tour
This document should give a first impression of the capabilities of Theorema 2.0.
The Theorema Interface
The user interface of Theorema 2.0 consists of:
- Theorema notebooks: These are Mathematica notebooks containing mathematical text. Theorema notebooks must be using one of the Theorema-specific stylesheets.
- The Theorema Commander: A graphical user interface supporting various interactions with the material contained in the notebooks.
Working in Theorema
"Working in Theorema 2.0" means
- writing structured mathematical documents in Theorema notebooks and
- setting up the current session,
These activities can be selected on the left margin of the Theorema commander. Depending on the activity, the top of the commander then displays the relevant
actions to be performed in the frame of the corresponding activity. In the picture above, one sees that the "Session"-activity consists of actions for "composing" the current session, "inspecting" the current session, and working with "archives".
Setting Up the Session
Creating a new notebook or opening an existing notebook should always be done using the buttons in the "compose"-action. Never use the standard
Mathematica procedures (through File-menu or
-O or
-N, or similar) for opening and creating notebooks. Why?
Read more ...This tutorial will be based on screen shots taken from the notebook
A First Tour and the
Theorema Commander, respectively.
For just browsing through the notebook you may click the link above and the notebook will open within the Help-browser and will be fully functional (after enabling dynamic objects), but it will not be possible to perform any actions in the notebook. In order to follow the examples in this tutorial "live" in your Theorema installation, please follow the instructions given at the beginning of the notebook
A First Tour.
If you follow the HTML-version of the documentation on the web, then
A First Tour links to an HTML translation of the Theorema notebook "A First Tour", which only shows the content but not the functionality that you would have when running the notebook in
Mathematica with Theorema installed. In general it is hard or next to impossible to resemble the interactive nature of Theorema notebooks in HTML.
Composing the Session: Theorema Environments
When working with Theorema, one will necessarily deal with formulas in one or the other way. In order to make a formula known to Theorema it must be evaluated in the frame of a Theorema environment (a definition, a theorem, a lemma, etc.). Theorema environments should be created using the buttons in the "compose"-action:
Place the cursor at the position in the notebook, where you want the environment to be inserted (cursor should be between two cells or at the beginning or end of the notebook), then press one of the buttons and a template for an environment of the chosen type will be inserted, e.g.
The environment consists of a
group of cells of different cell styles (opening the environment, environment header, etc.). The styles are important for the functionality of an environment, not only for their optical appearance.
- (a) The environment header contains the type of environment, e.g. "Proposition", and the ellipsis (...) indicate that a name for the environment can be given. As we will see later, names will help in the orientation. The entire content of the header is free-form, there are no syntactical rules. Also, the type of environment can be chosen freely, the buttons only give some suggestions. Use the ?-button if you want an environment that is not listed. The type of the environment implies no semantics, it is only eye-candy. Although it may make a difference for a human who reads the notebook, it makes no difference for the system, whether you write a formula in a definition or a theorem environment.
- (b) The formula itself goes in a cell of its own. Formula cells must have cell style "FormalTextInputFormula". An environment may contain more than one formula cells.
- (c) Every formula must have a label for later reference to that formula. Formula labels will be assigned from the cell tags of the cell, the "???" indicate that no label has yet been given. Use the standard Mathematica menu to edit cell tags and replace the "???" by the label of your choice. If you don't care about the label you may leave the "???", a new label will be generated automatically.
- (d) Grouping of the environment is important. The environment header groups until the end marker, there is an environment opener cell at the beginning and an environment closing cell at the end. Do not remove any of them.
- (e) Click the "
" in order to remove the environment, do not use Mathematica's native cut or delete.
Now place the cursor into the "
" in the formula cell and enter the formula. We suggest to use the buttons in the "compose"-action or the respective keyboard shortcuts:
For most of the language constructs available in the Theorema language we provide buttons to paste an expression template into the notebook. Buttons are grouped according to language categories (logic, arithmetic, sets, etc.), each button has a tooltip explaining parts of the expression and most importantly the keyboard shortcut for the respective expression. Every button has a corresponding shortcut.
In principle, a formula can also be pasted into the Theorema notebook. Note however, that an informally written formula bears the danger of getting a syntactically ill-formed expression when being pasted into
Mathematica. We therefore suggest
hierarchical formula input.
In order to make the formula known to Theorema it must be
evaluated (like
Mathematica input).
When the formula is evaluated, the label specified in the Cell Tags is put as a formula label into the right margin. The formula cell also has a "
" for deleting individual formulas. Like for environments, do not use
Mathematica's native cut or delete.
Proving
Once a formula is entered into Theorema, we are ready for proving it. "Proving" is the task of logical justification that a certain statement is true under certain assumptions. We call the statement under consideration the
proof goal and the assumptions the
knowledge (base). Now suppose we want to prove the formula labeled
(P or Q
if P then Q)
Q in Proposition (First Test, 2014), i.e.
First we change to the "Prove"-activity
to learn that the
actions necessary to prove something comprise the specification of the goal, the specification of the knowledge base, the declaration of built-ins, setting up the prover, submitting the prove task to the system, and finally inspecting the resulting proof. The actions on top should be run through from left to right thereby guiding the user through the proving process.
Selecting the Prove Goal
As indicated in the "goal"-action, for specifying the prove goal one only needs to select the cell in a Theorema notebook containing the formula to be proved, and the commander immediately displays the chosen formula.
Moving the selection to another formula will also change the selected prove goal until the button "OK, next ..." is pressed. This will
fix the proof goal no matter what is selected later in the notebook. For changing the goal, select another formula cell and press "OK, next ..." again. Fixing the goal will automatically take you to the "knowledge"-action.
Selecting the Knowledge Base
The knowledge base to be used by the prover is composed with the help of the
knowledge browser, which allows by simple mouse-click to select or deselect groups of formulas to go into the knowledge base. In the example above, we want an empty knowledge base, therefore we leave everything unchecked. The "OK, next ..."-button proceeds to the next action for selecting the available built-in operations. Alternatively, the next action can also be selected from the action-menu on top.
Selecting the Available Built-in Operations
Theorema built-in operations come into play, when computation is applied for formula simplification. The layout and functionality of the
builtin browser are similar to that of the
knowledge browser presented in the
"knowledge"-action above, using the checkboxes we can associate operations or entire groups of operations with their built-in meaning in the Theorema system. In proving we apply formula simplification by computation as soon as a new formula is generated. By default, only few operations are given a built-in meaning in proving. When doing a top-level computation in a Theorema notebook, the defaults are different, see Section
Computing below. In the current example, built-ins don't play a role, we can leave the defaults as they are. The "OK, next ..."-button proceeds to the next action for setting up the prover. Alternatively, the next action can also be selected from the action-menu on top.
Setting up the Prover
This is the central action in the "Prove"-activity, its purpose is to setup the prover to be used in the next proof. Essentially, a
prover in Theorema is a collection of logical proof rules (inference rules) together with a strategy how to apply the rules. The collection of available rules can be selected from a menu, and the "Proof Rules Setup" section then shows all rules hierarchically grouped in the
inference rule browser. The hierarchy is defined in the implementation of the rules and cannot be influenced by the user. The layout and functionality are similar to that of the
knowledge browser presented in the
"knowledge"-action above, it basically allows to activate and deactivate individual rules or entire groups of rules by simple mouse-click. In the current example, we deactivate "Prove by contradiction" because we assume that a direct proof would work. In general, we recommend to start a first proof attempt with the default settings, which should normally be a good starting point.
Next is the selection of the proof strategy. In the current prototype, we suggest to stay with the default "Apply once + Level saturation".
Finally, you can adjust limits for the prover's search depth (we take 20 instead of the default 30) and search time. A successful proof can be simplified by eliminating branches, steps, or formulas. Certain parts of the proving process may be guided
interactively (experimental feature!), and the
proof output may be adjusted. The "OK, next ..."-button proceeds to the next action for submitting the prove task. Alternatively, the next action can also be selected from the action-menu on top.
Submitting the Prove-Task
The "submit"-action shows a summary of all settings chosen in the "Prove"-activity. In case you want to modify something, go back to the respective action using the action-menu on top. If everything is fine, press the "Prove!"-button. Theorema will now try to generate a proof.
Inspect the Resulting Proof
While the proof is being generated the "inspect"-action displays the growing
proof search tree or parts of it as soon as it grows bigger (picture left). When the proof is finished, the Theorema commander shows the final proof tree (picture right) and some proof information is written into the Theorema notebook immediately below the environment containing the goal:
Most importantly, the ☑ indicates a successful proof (
would mark a failing proof) followed by "Proof of
<label> #<n>", where
<label> is the label of the proof goal and
<n> is a proof counter. Note that one goal can have more than one proof, e.g. using different provers, different settings, or different strategies. If there is already a proof for
<label> and we start a new attempt, then the
proof output section in the "prove"-action allows to decide whether one of the existing proofs should be replaced or a new proof is to be generated. Existing proofs are referred to by their counter.
Using the opener in the left margin, the cell group can be opened in order to show more
proof information. The information displayed there is not stored in the notebook, rather it is read from external files in the notebook's associated directory, see the
Theorema Session tutorial. Therefore, if you want to remove a proof, click the "
" in the right margin instead of using
Mathematica's native cut or delete, in order to allow Theorema to clean up the associated directory.
Finally, "Show proof" is a button that will open a new notebook containing the
nicely formatted proof.
The proof is presented in nested cells corresponding to the tree structure displayed in the "inspect"-action in the Theorema commander. Each branch of the proof corresponds to a cell group that can be collapsed and uncollapsed in order to show less or more details of the proof. All formula labels in the proof are hyperlinked to their first occurrence in the proof. Moreover, a tooltip shows the entire formula as soon as the mouse moves over a label. The proof notebook can be closed at any time and need not be saved, because it can easily be re-generated from the data in the associated directory by simply pressing "Show proof" again.
Computing
The essential thing to understand with Theorema computations is that the user has full control over the knowledge that is applied in a computation (like in a proof). That is, for a simple expression like e.g. '1+1' Theorema only computes the result '2' if we tell the system that '+' means the builtin addition of numbers. As an other example, if we have a definition for a function 'f' in the current session, we can compute 'f[3]' only if we allow the system explicitly to use the definition of 'f'. In this point, Theorema fundamentally differs from
Mathematica, where always all definitions in the current session are used in a computation.
The setup of user-defined knowledge and built-in operators is done via the "knowledge"- and the "built-in"-action in the "Compute"-activity, respectively.
Enter a New Computation
A computation is initiated by simply evaluating the input in a Theorema notebook. As opposed to
Mathematica, where input must be written in an input-cell, Theorema computation input must go into a cell with style "Computation". Such a cell can easily be created with the "New"-button in the "setup"-action. Note that when the cursor is located outside an environment and you just start typing, a new Computation cell will be created by default.
Checking the "Trace Computation"-box will record the steps during the computation for later visualization of the computation. Keep in mind, however, that tracing computations may slow down the computation.
Selecting the Knowledge Base
Again we refer to the notebook
A First Tour in order to follow the examples.
Suppose we have entered a new definition into the Theorema notebook:
This definition is not available for computations automatically.
Computation without knowledge
Only when activating the definition in the "knowledge"-action, it can be applied during computations. The knowledge browser in this action is a clone of the
knowledge browser for proving. Note however, that the knowledge settings for computation are independent from the settings for proving.
Computation with knowledge
Selecting the Available Built-in Operations
The computation above resulted in "True" because after expanding the definition of
<lex we were left with an existential quantifier with finite range. Theorema has built-in computation rules for expressions of that kind, and the "built-in"-action allows to configure, which of these should be used in a computation.
Again, the built-in browser is a clone of the
built-in browser for proving, only that the default settings for computation have most of the operators activated by default, whereas for proving most are deactivated by default. Like for the knowledge browser, the built-in settings for computation are independent from the settings for proving.
For demonstration purposes, we deactivate the existential quantifier in the Logic section.
Computation without built-in existential quantifier
The definition of
<lex is expanded and the variables
a and
b are substituted by the concrete tuples
1, 1, 1
and
1, 2, 0, respectively, but no further computations happen since the meaning of
is now not known. Certain subexpressions are evaluated, e.g.
1, 1, 1
simplifies to 3, but no further computations happen due to the presence of the variables
i and
j.
Some information related to the computation is written into the notebook directly following the result:
Using the opener in the left margin, the cell group can be opened in order to show more
computation information. The information displayed there is not stored in the notebook, rather it is read from external files in the notebook's associated directory, see the
Theorema Session tutorial. Therefore, if you want to remove a computation, click the "
" in the right margin instead of using
Mathematica's native cut or delete, in order to allow Theorema to clean up the associated directory.
Please have a look at the notebook
A First Tour in order to find more examples.
Solving
"Solving" is in our view the third basic mathematical task. In the current version of Theorema, solving is not yet integrated into the general user interaction model.
Customizing Theorema
The use of this activity should not need further explanation, except for maybe a word on the system language.
Changing the language in the system preferences changes not only the language of the user interface, but also the language used in natural-style proofs. After changing the language, the proofs need not be re-generated, since the proof objects, on which the display is based, are language independent. It suffices to re-display a proof in order to get it displayed using the currently selected language.
