Focus Windows:
A New Technique for Proof Presentation

Bruno Buchberger
(Implementation in Theorema: Florina Piroi)

RISC 
(Research Institute for Symbolic Computation)
Johannes Kepler University, Linz, Austria

Talk at the 2nd Workshop on Proving,Solving,Computing
Tokyo, Japan, Feb.17-18,2002
Organized by the SCORE Group,University of Tsukuba,Japan.

Copyright Note: The copyright is with Bruno Buchberger. Copying is permitted under the following conditions: The entire file is kept unchanged and complete. In particular, the copyright note must be included in the copy. If you copy the file, please send a mail to buchberger@risc.uni-linz.ac.at.

Proving, Solving, Computing and Theorema

Symbolic Computation = Automated Proving, Solving, Computing

B.B.: Invited talk at Multiparadigm Logic Programming Workshop, Sep. 15-16, 1996:

"Proving, Solving, Computing (Simplifying):
A Language Frame Based on Mathematica."

The three aspects of "symbolic computation" (automating mathematics):

Given (Subscript[Φ, x]), a formula with free variable x:

proving:         show that   (Subscript[Φ, x])  is true for all x  (in a given theory T).

solving:         find an x such that    (Subscript[Φ, x])  is true  (in a given theory T).

simplifying:   find a "simpler"   (Subscript[Ψ, x])  such that   (Subscript[Φ, x]) and (Subscript[Ψ, x]) are equivalent  (in a given theory T).

In other words:

proving:         handle  (Underscript[∀ , x])   (Subscript[Φ, x])  (in a given theory T).

solving:         handle   (Underscript[∃ , x])   (Subscript[Φ, x])  (in a given theory T).

simplifying:   handle    (Underscript[λ, x]) (Subscript[Φ, x])   (in a given theory T).

Note that the whole thing becomes challenging, interesting and practically useful only if we take into account the dependence of the proving, solving, and simplifying problem on the underlying theory. This theory may change many times during one proving, solving, or simplifying algorithm:

Proving (solving, simplifying) in T is often reduced to proving in some other P, solving in some other S, simplifiying in some other C. (This reduction is recursive.)

Example: Proving boolean combinations of equalities over the complex numbers can be reduced to the solvability of certain systems of multivariate polynomial equations over the complex numbers. The latter problem, by a certain simplification procedure (Groebner bases computation) can be reduced to detecting whether 1 is in the system.

Example: Proving certain formulae over real functions can be reduced, by the PCS method, to proving certain formulae over the real numbers. The latter problem can be reduced, by Collins' simplification method, to evaluating formulae on finitely many rational points.

Example: General first order proving in the empty theory can be reduced, by the resolution method, to the solvability of systems of clauses in the term algebra. The latter problem, by the unification algorithm - wich is a general simplification algorithm - can be reduced to detecting whether the empty clause is in the system.

Summarizing: Symbolic computation is a magma of provers, solvers, simplifyers for various theories.

Theorema

A system that tries to provide a growing magma of provers, solvers, simplifiers for various theories in one language and software frame.

Programmed in Mathematica but not relying on built-in knowledge of Mathematica.

An emphasis on the automatic generation of "human readable" proofs.

This talk: not on a particular prover, solver, or simplifyer but on the presentation of proofs.

The Problem

Understanding Proofs vs. Checking Proofs

Inventing and studying proofs has two aspects:

inventing / understanding the key ideas

checking the correctness

Both aspects are indispensable.

In this talk, I am only concerned with checking the correctness.

Checking Fully Displayed Proofs

Fully displayed proofs (in linear or any other form of presentation) are hard to check because

the formulae relevant in a proof step, typically, are scattered at quite distant places in the proof text

and, hence, one must "jump back and forth" and memorize formulae many times when checking proofs.

Note that this phenomenon is independent of the particular technique of displaying proofs.

Example

Remark

In a short talk, it is difficult to give good examples because the phenomenon becomes pronounced only in long proofs.

Definitions

We now give a couple of definitions in Theorema syntax:

Definition["is relation", 
      any[R], 
is–relation[
          R] : ⇔(R ⊆ 
              X\[Cross]X)]

'X' is a global constant.

Definition[\("is reflexive", 
      any[R], 
is–reflexive[
          R] : \(\(⇔\)\(∀ \+\(x ∈ X\)⟨x, x⟩ ∈ R\)\)\)]

Definition[\("is subsets set", 
      any[P], 
is–subsets–set[
          P] : \(\(⇔\)\(∀ \+\(p ∈ P\)p ⊆ 
              X\)\)\)]

Definition[\("is all nonempty", 
      any[P], 
is–all–nonempty[
          P] : \(\(⇔\)\((∀ \+\(p ∈ P\)p ≠ {})\)\)\)]

Definition["class", 
      any[R, x], 
class[R, 
          x] := {y (Underscript[\[VerticalSeparator] , y ∈ 
                  X])⟨y, x⟩ ∈ 
              R}]

Definition["factor set", 
        any[R], 
factor–set[
            R] := {class[R, x] (Underscript[\[VerticalSeparator] , x])x ∈ X}];

Lemma

Lemma["example", 
      any[R], 
(is–relation[R] ∧ 
            is–reflexive[
              R]) \[Implies]  (is–subsets–set[
              factor–set[R]] ∧ 
            is–all–nonempty[factor–set[R]])]

Prover Call

Prove[\(Lemma["example"], \ 
      using -> ⟨Definition["factor set"], 
          Definition["class"], Definition["is relation"], 
          Definition["is reflexive"], Definition["is subsets set"], 
          Definition["is all nonempty"]⟩, 
by -> SetTheoryPCSProver\)]

This call to Theorema generates, fully automatically, the following proof (including  the intermediate explanatory English phrases):

Proof

The Problem

Design a presentation technique for proofs that, in each proof step, has all the relevant formulae "in the focus of the reader".

A Solution

A Note

Note that no solution is possible for proofs on paper or blackboard.

However, when proofs are available as data objects in machines (as this is the case with proofs generated by automated theorem provers like Theorema), a solution is near at hand.

Solution

In a post-processing step, we go over the proof object and generate a sequence  of "focus windows".

Proof Objects and Proof Situations

Proof object: nested tree of proof situations.

Proof situation: consists of

current goal formula

current knowledge base

indication of inference rule used together with reference to the relevant formulae in the knowledge base.

Focus Windows

The focus window of a proof step displays the current goal and the relevant formulae.

Displaying a focus window proceeds in two phases:

attention phase: the current goal and the relevant formulae are displayed

transformation phase: in addition, the resulting new formulae (goals and / or new knowledge) are displayed.

Example

Prove[\(Lemma["example"], \ 
using -> ⟨Definition["factor set"], Definition["class"], 
          Definition["is relation"], Definition["is reflexive"], 
          Definition["is subsets set"], 
          Definition["is all nonempty"]⟩, 
by -> 
        SetTheoryPCSProver, 
showBy -> FocusWindows\)]

This Theorema call, with the option 'showBy' set to 'FocusWindows', produces now the following alternating sequence of attention and transformation windows, each of wich should be easy to study because each attention window contains all the information relevant in the respective proof step and the successive transformation then shows, in addition, the next formulae generated in this step.

Initialization Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Branch 1

Next         Previous        Done

Branch 2

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Branch 1

Next         Previous        Done

Branch 2

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Attention Window

Next         Previous        Done

Transformation Window

Next         Previous        Done

Conclusion

Next version of the implementation of the Focus Windows technique in Theorema: Will combine the usual linear presentation of proofs with "focus windows on demand".

We will also implement a feature by which the size of the  font in a proof window will decrease to such an extent that the entire text in a focus window always fits into the physical screen.

We learned that the focus windows proof presentation is also a very useful tool in the phase of developing and debugging new automated provers.

The notion of focus window also has theoretical bearing:

It is another way of characterizing the inference rules of special inference systems (for special mathematical theories).

Also, focus windows contain exactly the information necessary in the "cascading technique" (= analyze failing proofs and invent useful lemmata) of Theorema.

References

The following papers on Theorema, the focus window technique, and various issues referred to in the talk (e.g. the cascading technique and theory exploration) can be downloaded from my home page:

http://www.risc.uni-linz.ac.at/people/buchberg/

B. Buchberger.
Focus Windows: A New Technique for Presenting Mathematical Proofs (in Automated Theorem Proving Systems).
Theorema Technical Report, 2000-01-30, Research Institute for Symbolic Computation, Johannes Kepler University, A4040 Linz, Austria, 19 pages.

B. Buchberger.
Theory Exploration with Theorema.
In: Proceedings of SYNASC 2000 (2nd International Workshop on Symbolic and Numeric Algorithms in Scientific Computing), Oct.4-6, 2000, Timisoara, Rumania, (T.Jebelean, V.Negru, A.Popovici eds.), Analele Universitatii Din Timisoara, Ser. Matematica-Informatica, Vol.XXXVIII, Fasc.2, 2000, pp.9-32.

B. Buchberger.
Theorema: Extending Mathematica by Automated Proving.
Invited talk at PrimMath 2001 (The Programming System Mathematica in Science, Technology, and Education), University of Zagreb, Electrotechnical and Computer
Science Faculty, September 27-28, 2001.

B. Buchberger.
Logicographic Symbols: A New Feature in Theorema.
In: Symbolic Computation - New Horizons (Proceedings of the 4th International Mathematica Symposium,Tokyo Denki University, Chiba Campus, Japan, June 25-27, 2001), Tokyo Denki University Press, 2001, pp.23-30.

B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, W. Windsteiger.
The Theorema Project: A Progress Report.
In: Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS 2000, Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, August 6-7, 2000, St. Andrews, Scotland, M. Kerber and M. Kohlhase eds.), A.K. Peters, Natick, Massachusetts, pp. 98-113. ISBN 1-56881-145-4.