On the Design of Mathematical Concepts
This work was supported by European Commission IHP Calculemus Project grant HPRN-CT-2000-00102.

Manfred Kerberⁱ

Martin Pollet^i,ii

ⁱⁱFachbereich Informatik
Universität des Saarlandes
66041 Saarbrücken, Germany
http://www.ags.uni-sb.de/~pollet

ABSTRACT

That foundational systems like first-order logic or set theory can be used to construct large parts of existing mathematics and formal reasoning is one of the deep mathematical insights. Unfortunately it has been used in the field of automated theorem proving as an argument to disregard the need for a diverse variety of representations. While design issues play a major rôle in the formation of mathematical concepts, the theorem proving community has largely neglected them. In this paper we argue that this leads not only to problems at the human computer interaction end, but that it causes severe problems at the core of the systems, namely at their representation and reasoning capabilities.

1.  Introduction

For instance, Pat Hayes said in 1974 ([Hayes74] quoted from [Brachman85b, p.18]):

In this paper we try to clarify why the argument, although it may be technically correct, is pragmatically flawed and has led to very negative consequences. The argument is pragmatically wrong, since it is meant to say "Your system X is redundant and uninteresting, since we have system Y already, which suffices for everything you want to do." Since this argument was widely accepted the focus in the field was set much too narrow on the study of foundational systems. For other communities, our observations in this paper may be trivial.

Of course there are exceptions and we claim in no way that we are the first to have a look at this relationship of mathematical practice and fundamental systems. In this paragraph we do not claim to give a comprehensive overview of this type of work. We just mention some work in this direction, which we think provides very important starting points to the support of the design of mathematical concepts. In Automath, N.G. de Bruijn developed the idea of a mathematical vernacular [Bruijn94], which should allow to write everything mathematicians do in informal reasoning, in a computer assisted system as well. In this tradition, Hugo Elbers looked in [Elbers98] at aspects of connecting informal and formal reasoning, in particular the integration of computations in formal proofs. Francis Jeffry Pelletier [Pelletier91] as well as Henk Barendregt and Arjeh Cohen [Barendregt01] discuss related philosophical questions on the nature of proof. Proof planning [Bundy88] in general can be viewed as an attempt to simulate informal reasoning (and integrate it with formal reasoning). Following this paradigm, Alan Bundy made first steps towards a Science of Reasoning [Bundy91], which goes beyond a narrow focus on a particular calculus. Ursula Martin took in [Martin99] a close look at the mathematical practice and its relationship to computer algebra and computer-assisted reasoning. Michael Beeson presented in [beeson98] a system that combines deductive and computational reasoning steps. He proposed to use the mathematical standard for checking the correctness of proofs generated by the system, namely peer reviews.

We are not aware, however, of work in which the design process in mathematics is compared to the design possibilities of computer based mathematical support systems. In this paper, we look at design problems, which current automated reasoning systems suffer from, and relate them in the rest of this introduction to an old debate in mathematical philosophy, which summarises the relationship between foundational systems and informal systems very well.

We do not doubt that one of the deepest insights in the foundations of mathematics resulted from the epochal work by Bertrand Russell and Alfred North Whitehead. Russell articulated the idea in the Principles of Mathematics [Russell03] namely, to reduce mathematics to formal logic, and carried it through together with Whitehead in the famous Principia Mathematica [Whitehead10] - a work often quoted and seldom read. Russell was at this time also in inspiring discussions with Ludwig Wittgenstein and strongly acknowledges Wittgenstein's contribution to his thoughts. He writes in [Russell18] (quoted from the reprint in [Russell56, p.178]):

Although there is evidence that Wittgenstein shared Russell's view, he later took the opposite stance and attacked Russell's approach. In particular he discusses the important notion of proof (quoted from [Wittgenstein56, p. 143]):

We try to exemplify in the rest of the paper why these matters are crucial for automated theorem proving systems. One important issue is that of acceptance among mathematicians. Current automated theorem provers do not find acceptance among mathematicians, while computer algebra systems do. In many computer algebra systems things are as they should be, as an inexperienced but mathematically educated user would expect them to be. That is, these systems are typically well-designed. In automated theorem proving systems they are typically not as they should be, not as an inexperienced user would them expect to be. We will argue that this is not just a deficiency of the interface, but that the problem with automated theorem provers is much deeper, it goes to the core of these systems, namely to the formal representation of mathematical knowledge and the reasoning that can be performed with this knowledge.

2.  Design Issues Exemplified with Multiplication Tables

In this section we want to have a close look at one particular example of a mathematical concept which is carefully designed. Before we do so, let's have a more general look at design issues. Donald Norman gives a fascinating introduction into "The Design of Everyday Things." His insights are of a very general nature and we will see that the principles for good design hold in mathematics as well.

Although Norman does not relate design to mathematics, most observations can be translated to a mathematical context. For instance, design principles allow us to answer questions like "Why and how do we find a proof without major search effort, although it is a difficult one and we don't know it?" Norman states four principles why we get certain things right, although we don't know precisely what to do [Norman98, p.55]:

1. Information in the world. Much of the information a person needs to do a task can reside in the world. Behavior is determined by combining the information in memory (in the head) with that in the world.
2. Great precision is not required. Precision, accuracy, and completeness of knowledge are seldom required. Perfect behavior will result if the knowledge describes the information or behavior sufficiently to distinguish the correct choice from all others.
3. Natural constraints are present. The world restricts the allowed behavior. The physical properties of objects constrain possible operations: the order in which parts can go together and the ways in which an object can be moved, picked up, or otherwise manipulated. Each object has physical features - projections, depressions, screwthreads, appendages - that limit its relationship to other objects, operations that can be performed to it, what can be attached to it, and so on.
4. Cultural constraints are present. In addition to natural, physical constraints, society has evolved numerous artificial conventions that govern acceptable social behavior. These cultural conventions have to be learned, but once learned they apply to a wide variety of circumstances.

We argue that humans make use of such principles, not only in their relationship to everyday objects like door handles, but also in their relationship to mathematical objects like multiplication operators. However, conventional theorem proving systems do not. We will take a closer look at multiplication tables, a concept that seems on a first view easy, and on a second difficult to model in existing theorem proving systems. Multiplication tables are part of rigorous mathematics in the sense that they appear not only as comments or illustrations in mathematical textbooks, but are usually introduced in definitions and their properties are stated as theorems.We use here the word "rigorous" and not "formal" in order to distinguish it from "formal logic" and mechanical systems. Mathematicians would probably use the word "formal," since they are happy with these concepts as a level of formalisation that clarifies concepts unambiguously. We believe that the features of the concept "multiplication table" as well as those we present in the next section are not only a matter of presentation but that they are used to encode and retrieve information about mathematical concepts in an efficient way and that they ease the actual process of finding and presenting proofs.

The table has its own notion of well-formedness, that is, all d_i have to occur and have to be different, the table must be fully filled. Here you find Norman's principles 1, 3, and 4. Multiplication tables are designed in a way that their structure puts "information in the world" that makes it difficult to violate well-formedness. It is hard to imagine when you've got the task to define a specific operation starting with an empty multiplication table that you forget a case, since that would leave a hole in the structure. The table itself is of the form that it constrains the possibilities. For instance, it is impossible to enter more than one entry per field. This prevents any over-specification of o . Furthermore, although the order of the d_i in the columns and rows could in principle be different, cultural conventions prevent that.

Note that there are particular reasoning methods connected to the representation. To check the basic property of closedness, one has to go through the elements of the table and check whether for all elements holds c_ij in {d₁,... ,d_n}. The commutativity of o is checked by verifying that the table is symmetric with respect to the diagonal. This intuitive form of reasoning depends on the cultural convention to use the same order for rows and columns. Another cultural convention is to write a (potential) unit element as first element (or second element in the presence of a zero, which typically goes in the first place). With this convention, it is checked that d₁ is a unit element by establishing the equality of the columns under o and d₁ and the rows right to o and d₁. Inverse elements can be checked by establishing that each column and each row contain the neutral element exactly once. These reasoning patterns follow partly the design principle number 2, since they are natural and easy to reconstruct. From the group properties only associativity requires a logic level proof.Surely, for people experienced with this type of proof, there isn't anything to prove anymore, but it boils all down to trivial computations, which according to the Poincaré principle [Barendregt01] can be considered as not being a part of the proof. This is different for beginners, whose perspective we have taken here.

Of course, it is possible to define the same operation in a logic, possible formalisations are for example:

• First order: extend the signature by a function constant o and add the assumptions d₁ o d₁= c₁₁ & d₁ o d₂=c₁₂& ... & d_n o d_n= c_nn.
• Higher order: use the description operator The description operator i returns the element of a singleton. i y.P[y] denotes the unique element c such that P[c] holds, if such a unique element exists. to define the operation as
  o  <-> lambda x.i y. (x=(d₁,d₁)& y=c₁₁)v... v(x=(d_n,d_n)& y=c_nn).

Although, the higher order formalisation of the operation seems preferable over the first order one since it encodes o as one compound object, here as well it is hard to recognise what kind of function is encoded. Actually, there is a proof obligation to be shown in an application of the function to arguments, namely that there is really a unique element with these properties.

While programming languages like Caml (see e.g., http://caml.inria.fr/) foster for the transition between different data structures, this is typically difficult in deduction systems. We will briefly discuss the little theory approach in IMPS [Farmer92] later (see section 4.2).

3.  Mathematical Representations

3.1.  Matrices

In principle matrices over a field F can be represented in logic by functions from an index set into F. However, this representation does not lend itself to the definition of multiplication of matrices in which product elements are calculated by traversing the left matrix left-right and the right matrix of the product top-down. The generalisation of this principle makes it easy to establish the relationship accounted for above. Furthermore the explicit matrix representation exhibits advantages mentioned above for multiplication tables.

Note that matrices are available in Computer Algebra Systems (CASs) as primitives and that direct manipulations are possible. This, however, does not make it obsolete to introduce them directly into automated theorem proving systems as well. For instance, the matrices used in the equation above cannot be easily defined in a CAS, since they represent more than one instance, they are generalised matrices representing any matrix that has the same `form.' Establishing the equation itself cannot be done by computation, but requires reasoning. Once established it can become a further computation rule.

3.2.  Dynamic Representations

The first formalisation eases the possibility to inherit properties of subsumed concepts with group(G, o ) ->  monoid(G, o ). The latter formalisation makes the unit elements and inverse elements directly accessible but already contains the uniqueness of the inverse element of an element in form of the inverse function. The process of the actual exploration of basic principles of group theory that starts with the tuple (G, o ) and later introduces the neutral and inverse elements as useful parameters of the concept can hardly be modelled in current automated reasoning systems. Rather it is necessary to choose one formalisation and to stick to it. This way it is not only the case that the introduction of a concept cannot be modelled adequately, but perhaps more seriously re-representations of concepts are not supported. However, while one representation may be best suited for one task, it may turn out to be unsuitable for a different one. In the latter situation mathematicians change representations. Different formalisations model different views on something that is one single mathematical concept to a mathematician. If a mathematician had to use one of the standard theorem proving systems, he or she would need to know in advance which choice of representation to make, since the choice of a good formalisation is crucial for the success. But how do you know which formalisation is best, when you start to explore something?

Another example of dynamic re-representation, which is very simple, but for which the different reasoning complexities are striking, is when associativity holds for an operation +. Once associativity is established, no mathematician would still use brackets, but the notation for a term like ((1+x)+y) would change to 1+x+y. The property is encoded into the notation and can be retrieved from the given term. On a reasoning level this simple shift in representation can make a dramatic difference. For a term with n+1 summands there are [1]/[n+1]

3.3.  Change of Representations

• functions: Given an Euclidean space R with a metric function | |:R x R->R then for each pair A,B in R of disjoint points there exists exactly one distance preserving function g_A^B:R->R with g(0)=A, g(|AB|)=B. With the help of this function the lines in Euclidean space can be interpreted as images of the real numbers. Notions of the real numbers, as intervals, correspond to notions in the abstract Euclidean space, namely line segments.
• representation theorems: Poincaré's model for the hyperbolic plane, where a line has infinitely many parallel lines through one point, is a unit disk, where circle segments correspond to hyperbolic lines. With this representation it becomes possible to re-represent constructions in the hyperbolic plane as constructions in the Euclidean plane.
• theory change: Geometric constructions can be represented as field extensions. The possibility to construct a square equal in area to a circle using compass and ruler can be re-represented to the question whether pi belongs to a particular class of algebraic numbers (which it does not since it is transcendental).
• inheritance: The properties of monoids and groups are inherited by the multiplicative and additive substructures of rings and fields.
• diagrams: P in [AB],B in [AQ] ->  P in [AQ],B in [PQ] which is obvious when this situation is expressed in a diagram:

• Cartesian geometry: arithmetic representation for geometry. This makes it possible to reduce geometrical problems to arithmetic problems and solve them arithmetically. This is actually the starting point of Descartes' idea to take arithmetic as a foundational system so that all problems should be translated to arithmetic and then solved by equation solving.
• set theory: mathematical concepts are representable as sets. Set theory is another foundational system on which most of mathematics can be based in principle.
• group theory: the group concept can be used to represent geometric transformations, permutations, and the solvability of polynomials.

Certain forms of representations are very important to form new concepts. The theorem that every permutation can be decomposed into transpositions, that is, can be represented as a product of transpositions, makes the definition of even and odd permutations suggestive. It is hard to imagine how to define the concept without this particular representational form. Once these concepts have been formed they become the starting point for the introduction of other concepts like the alternating group.

Let's look at a different example, the concept of real numbers. Real numbers can be defined as Dedekind cuts or Cauchy sequences. However, Cantor's second diagonalisation proof that the reals are uncountable is difficult to imagine without having the representation in the decimal (dual, or another) number system.

Often the opposite of a change in the representation happens in mathematics, that is, so-called overloading is used. The use of the same notation for different concepts, e.g. | | in the example above for the concept of distance, + for operations that behave like the well-known addition on natural numbers, etc. Even formally incorrect notation, as equality for isomorphisms, is used to enable the transfer of knowledge from a known concept to a new concept. Certain sort and type systems allow for some kind of overloading, but they do not offer the kind of knowledge transfer that humans achieve this way in using overloaded symbols in an analogical way.

3.4.  Limited Coverage of Mathematical Activities by Logic

But even at the level of problem formulation, it is not always possible to apply a formal system in a straightforward way. Let's look for instance at the mathematical task (provided in some context): "Determine the maximum of f(x) in the interval [a,b]." Does the obvious formalisation "EXISTS_{x in [a,b]} max(f,x)" reflect the meaning of the sentence? Not necessarily, assume somebody comes up with the argument "Since f is a continuous function on a compact interval it has a maximum." This might be a correct argument to prove the logical formulation but it would not solve the original task. On a closer look adequacy of the logical statements depends on the logic used. If interpreted in a constructive way the logical formulation is adequate; if interpreted classically it is not. While there are constructive and classical systems around, it seems to be inappropriate that one has to decide for a constructive system once and for all, in order to be able to formulate a standard task like the one above.

While one can hardly cover all aspects of mathematics in a computer-based system, it seems for many applications - like the recently emerging applications in education - important to find a coverage which is as broad as possible.

3.5.  A `Natural' Calculus

The strength of a formal system can be measured by the de Bruijn factor, that is, the ratio of the length of the proof in the formal system compared to its version in a mathematical textbook.The notion is not without problems, since mathematical proofs are not standardised with respect to their detailedness. Furthermore there are other aspects for the quality of a proof than its length. A reassuring observation is that in the experiments with Automath and Mizar the de Bruijn factor remained constant for the proofs of a wide range of differently complex theorems.

Even if we agree with the conclusion that the proofs constructed in formal calculi are already in principle an approximation of standard mathematical proofs, it is important to note that such a comparison is based on the output of mathematical work, the language used by mathematicians to communicate proofs in textbooks and articles. While a comparison of such completed proofs, proofs after all search is finished may be interesting, they often do not resemble the proof construction. As an example look at standard epsilon-delta-proofs. In the proof construction you compute a sufficient criterion on delta, choose delta as a function of epsilon and than you prove that with this delta the difference of the function values is indeed smaller than epsilon. In a finished proof a crucial part of the proof construction, namely the construction of delta, is redundant and hence not presented. For this reason it is impossible to understand prima facie why delta has been selected as it is.

Traditionally, the formulations of final proofs are minimalist and mathematicians repress their original ideas, even the order of steps can be different, in favour of an objective rigorous style. As Pólya [Polya54, p. vi], pointed out:

The `demonstrative reasoning' corresponds to a formulation in reasoning steps that were investigated by logicians. In this sense current deduction systems are suitable as proof checkers for existing and well-understood parts of mathematics but lack to act as proof assistants for the exploration and construction of new mathematical knowledge. How can `plausible reasoning' be modelled? Proof planning follows the paradigm of proof search on an abstract level and can be seen as an important step into this direction. But as described in [omegafuture] even proof planning depends on structural restrictions of the underlying calculus and uses a formal language as the only representation for mathematical concepts.

There might be the view that we can come up with a more powerful logic which provides the best possible representation. Marvin Minsky gave a strong argument why this wouldn't be the case in artificial intelligence in general, but why multiple representations are necessary. He recommends [Minsky95]:

As we have seen for multiplication tables different types of representations allow for specialised and efficient reasoning methods connected to them, opposed to search on the logic level. Mathematicians carefully design their concepts to keep the search spaces small. We need to understand this aspect of mathematical reasoning much better in order to understand the versatility of the reasoning capabilities of human mathematicians.

Historically the development of many concepts went the way that certain meta expressions were introduced, which were later reified and become object expression. The development of number systems might illustrate this. Having natural numbers and fractions, irrational numbers and negative numbers as well were considered as odd ones out, which only later became first class citizens. Then imaginary numbers were the odd ones and negative square roots were considered as strange entities which were used only for convenience. Likewise, functions were first concrete in nature, and only much later it was possible to speak about them.

4.  Representations of Mathematics on Computers

4.1.  Sorted Extensions to Logic

The reason for the smaller search space is due to a better design realised by the sorted system. Although the formalism of sorted logic is equivalent in strength to the unsorted one, a concrete formulation (which makes use of sorts in a non-trivial way, that is, whose relativisation is not equal to itself) is not. It is actually weaker, since certain things can not be derived in sorted logic which can be derived in unsorted logic (concretely, formulae like human(1) -> mortal(1) are syntactically possible in unsorted logic, but the equivalent is rejected in sorted logic). To generalise this observation: A particular design is better than an alternative one if certain redundant, or heuristically uninteresting derivations cannot be made.

The integration of sorts in a system also demonstrates how subtle design issues can be. We can't discuss this in detail here, but we will give some indication. It should be noted that sorts are not necessarily exclusively beneficial.For a detailed discussion why sorts/types may be harmful see [Lamport95]. If we take standard order-sorted logic we have for each relation like human and mortal to decide whether we want to formalise it by a sort symbol or by a predicate symbol. If we want to prove some statement like NOT human(Pegasus), we cannot formalise human as a sort symbol. This is a serious flaw in standard sort systems, also it is not possible to model the genesis of concepts in an adequate way. In order to perform the reasoning above we need to know socrates in human a priori. It is not possible to infer that Socrates is a human being later in the reasoning process. This unduly limits the flexibility of the system. Ideally you would want to have the advantages of a sorted formulation whenever possible, but also benefit from the flexibility of the unsorted formulation when necessary. To our knowledge only Christoph Weidenbach's system [Weidenbach93] offers these possibilities.

4.2.  Little Theories

4.3.  Data Structures in Computer Algebra Systems

4.4.  Data Structures for Reasoning

Mateja Jamnik describes in [JamnikBook] a diagrammatic representation for theorems and inference steps based on this data structure that allow to infer theorems in arithmetic. The proofs constructed in the diagrammatic representation can be translated to proof planning and then formally verified with a theorem prover.

These examples are important in our context since they show that at least for particular domains it is possible to build special reasoners for diagrammatic reasoning which are distinct from a purely logic based system, but which can be formally linked to such a system. An adequate data structure for diagrams seems to be the key point for the success of both approaches. Only this data structure allows the implementation of an efficient inference mechanism.

5.  Discussion

In this paper, we presented aspects of mathematical representations that we think are highly relevant for mathematical theorem proving and that can - if at all - be implemented in traditional theorem proving systems only with great difficulty. We think that the lack of acceptance of theorem proving systems (compared with the success of computer algebra systems) is also due to these shortcomings. Deduction systems offer - compared to computer algebra systems - only limited added value: formal correctness, but at a very high price, namely a significant overhead to formulate and prove mathematics. While the production of a large body of formally correct proofs for known theorems does usually not correspond to the research interests of mathematicians, the exploration of new problems is not very well supported as we observed in section 3.

Current deduction systems ideally offer the potential benefit that they can relieve users from the tedious task of checking trivial subproblems, so that the human can concentrate on the interesting parts of the problem. In practice, however, it is typically more work even for an experienced human mathematician to formulate the problems in the first place so that an automated theorem prover can prove them than to do the job directly him/herself. We think, when a theorem proving system wants to have a real application as either a proof assistant or a proof tutor, it has to take care about the representation that is used by mathematicians.

The mathematical representation is not only important for the user interface and presentation of proofs, but for theorem proving itself, since the representation is used to optimise problem solving and the transfer and access of knowledge. The observations presented in section 3 reveal that mathematical knowledge is highly structured and special representations are important for mathematical problem solving. Data structures that realise these aspects may allow for the definition of detailed problem classifications for which special but efficient mechanisms can be found. In sections 4.1 and 4.4 we gave examples for data structures and implementations of this kind. Mathematical representation appears furthermore to be dynamic and flexible. Modelling this flexibility is on the one hand important for the user interface, because it would give the choice for a representation to the user. On the other hand, this flexibility is the key point for the combination of different representations. We have summarised some approaches to good design in section 4. More work in this direction is necessary to offer well-designed tools to mathematicians and other people interested in computer assisted mathematics. While certain parts might turn out to be straightforward other aspects will require a much deeper understanding. To give one example for the size of the task, if we wanted to integrate multiplication tables as a primitive in automated reasoning systems, it should be relatively easy to offer concrete multiplication tables (or matrices) with all the advantages mentioned in sections 2 and 3 (as it is relatively easy to offer order-sorted sorts). However, it will be difficult to offer general type multiplication tables (or matrices) which contain ellipses, and flexible ways to reason about them. Human beings have an amazing capability to reify structures in their space of discourse. We seem not to have yet a deep understanding of these capabilities.

This paper compared approaches in mathematics and in existing theorem proving system. We did not aim to offer solutions, but want to conclude with some thoughts how a strong reasoning system would have to look like to model mathematical practice more adequately. Such a system should firstly be its own meta-system, so that it can speak about itself (care about paradoxes has to be taken). Secondly, the definition of mathematical structures as well as establishing their formal relationships would have to be provided by such a system. Thirdly, a graphical user interface should facilitate the possibility to relate mathematical structures to a form, which is familiar to mathematicians. Particularly important are in this context spatial and diagrammatic representations. While there are approaches to all these points, to our knowledge no single system offers yet an integrated flexible approach.

Acknowledgements

References

• [Barendregt01] H. Barendregt and A.M. Cohen. Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants. Journal of Symbolic Computation, 32(5):3-22, 2001.

• [beeson98] M. Beeson. Automatic generation of epsilon-delta proofs of continuity. In J. Calment and J. Plaza, editors, Artificial intelligence and symbolic computation, pages 67-83. Springer Verlag, Berlin, Germany, LNCS 1476, 1998.

• [omegafuture] C. Benzmüller, A. Meier, E. Melis, M. Pollet, J. Siekmann, and V. Sorge. Proof planning: A fresh start? In M. Kerber, editor, IJCAR-Workshop: Future Directions in Automated Reasoning, pages 30-37, Siena, Italy, 2001.

• [Brachman85b] R. Brachman and H. Levesque, editors. Readings in Knowledge Representation. Morgan Kaufmann Publishers, Los Altos, 1985.

• [Bruijn94] N.G. de Bruijn. The mathematical vernacular, a language for mathematics with typed sets. In R. Nederpelt, J. Geuvers, and R. de Vrijer, editors, Selected Papers on Authomath, pages 865-935. Elsevier, North-Holland, Amsterdam, 1994.

• [Bundy88] A. Bundy. The use of explicit plans to guide inductive proofs. In E. Lusk and R. Overbeek, editors, Proc. of the 9th CADE, pages 111-120, Argonne, Illinois, USA, 1988. Springer Verlag, Berlin, Germany, LNCS 310.

• [Bundy91] A. Bundy. A science of reasoning. In Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991.

• [BundyRichardson99] A. Bundy and J. Richardson. Proofs about lists using ellipsis. In H. Ganzinger, D. McAllester, and A. Voronkov, editors, Proc. of the 6th LPAR, pages 1-12. Springer Verlag, Berlin, Germany, LNAI 1705, 1999.

• [Elbers98] H. Elbers. Connecting Informal and Formal Mathematics. PhD thesis, Eindhoven University of Technology, 1998.

• [Farmer92] W. Farmer, J. Guttman, and F. Thayer. Little theories. In D. Kapur, editor, Proc. of the 11th CADE, pages 567-581, Saratoga Springs, New York, USA, June 1992. Springer Verlag, Berlin, Germany, LNAI 607.

• [Hayes74] P. Hayes. Some problems and non-problems in representation theory. In Proc. of the AISB Summer Conference, pages 63-79, Sussex, 1974.

• [JamnikBook] M. Jamnik. Mathematical Reasoning with Diagrams: From Intuition to Automation. CSLI Press, 2001.

• [KoedingerAnderson90] K. Koedinger and J. Anderson. Abstract planning and perceptual chunks: Elements of expertise in geometry. Cognitive Science, 14:511-550, 1990.

• [Lamport95] L. Lamport. Types are not harmless. Technical report, 1995.

• [Martin99] U. Martin. Computers, reasoning and mathematical practice. In U. Berger and H. Schwichtenberg, editors, Proceedings of the NATO Advanced Study Institute on Computational Logic, Marktoberdorf, Germany, July 29 - August 10, 1997. Springer Verlag, 1999.

• [Minsky95] M. Minsky. Future of AI technology. Toshiba Review, 1992. http://web.media.mit.edu/~minsky/papers/CausalDiversity.html.

• [Norman98] D. Norman. The Design of Everyday Things. The MIT Press, London, 1998.

• [Pelletier91] F.J. Pelletier. The philosophy of automated theorem proving. In John Mylopoulos and Ray Reiter, editors, Proc. of the 12th IJCAI, pages 538-543, Sydney, 1991. Morgan Kaufmann, San Mateo, California, USA.

• [Polya54] G. Pólya. Mathematics and Plausible Reasoning. Princeton University Press, New Jersey, USA, 1954.

• [Polya62] G. Pólya. Mathematical Discovery - On Understanding, Learning, and Teaching Problem Solving. Princeton University Press, New Jersey, USA, 1962/1965.

• [Russell03] B. Russell. The Principles of Mathematics. George Allen & Unwin Ltd, London, UK, 2nd edition, 1937 edition, 1903.

• [Russell18] B. Russell. The philosophy of logical atomism. The Monist, 28/29:495-527/32-63,190-222,345-380, 1918/1919. republished in [Russell56, p.177-281].

• [Russell56] B. Russell. Logic and Knowledge. Allen & Unwin, London, 1956.

• [Weidenbach93] C. Weidenbach. Extending the resolution method with sorts. In Proc. of the 13th IJCAI, pages 60-65, Chambéry, France, 1993.

• [Whitehead10] A.N. Whitehead and B. Russell. Principia Mathematica. Cambridge University Press, Cambridge, UK, 1910.

• [Wittgenstein56] L. Wittgenstein. Remarks on the Foundations of Mathematics. Basil Blackwell, Oxford, England, third edition edition, 1956.