Goal XXXXXXXXXXXXXXXXX * Support "doing" mathematics by computer using one interface * All phases of doing mathematics, see "creativity spiral", should be supported * Including the phases of studying, teaching, publishing, documenting, storing mathematics * The main missing link is support of proving * "Combining computer algebra and theorem proving" is not a goal in intself. * Rather, combining computer algebra and theorem proving is the method how to achieve the goal of supporting all phases of doing mathematics. * One interface for one person * There may be many different interfaces in different "combined systems". However, as a user, when I log into "my system" I would like to have one interface that guides me through the use of, maybe, many different individual systems that are accessible - at my site or through the web - from my uniform interface. * The question is not: "Human proving" (done by ingenious "pure mathematicians") against "machine proving" (done by dull "computer scientists"? Who is better? * "Machine proving" is also human proving because the prover was designed by a human * "Machine proving" (in a certain area) should be called "algorithmic proving" or systematic proving * It needs the best mathematicians to invent systematic proving procedures for certain areas * The difference between human proving and machine proving is exactly the same as between inventing the solution of the equation a . x = b by for each given a, b individually versus determining x by an algorithm whose correctness has been proven once and for all * Computer-supporting proving is just one of the natural steps in automating mathematical problem solving by more and more times through the creativity spiral on higher and higher levels Problems XXXXXXXXXXXXXXXXXXX Do we need a common logic frame? Do we need a common syntax frame? How to combine systems? How to master complexity of knowledge? How to make computer supported proving efficient? A Common Logic Frame? XXXXXXXXXXXXXXXXXXXXXXXXX Seems to be important and non-trivial for theoretical reasons Not so important for the practical aspects A common notion of a proof? XXXXXXXXXXXXXXXXXXXXXXXXXXXXX Seems to be a difficult problem but is not! A Notion of Proof and Proof Object Proof objects are the things which we exchange and trade Various actors can work on the proof objects, e.g. pretty-printers, natural language presentators, algorithm extractors, proof simplifiers etc. Structure of proof objects --------------------------- < Echo input, proof steps, result > Echo input: < prover used , formula to be proved, knowledge based used> ----------------- The information "prover used" is crucial for theoretical and practical purposes: --------------------- avoids discussion on the notion of a proof allows object oriented approach e.g. allows combination of the results of individual provers e.g. allows the invocation of actors for the particular class of proof objects Proof steps: a sequence of proof objects of the same structure --------------------- Result: "proved" | "disproved" | open problem ------------------- A Common Syntax Frame? xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx Most probably not. There are many tools around for transforming formulae in various disguises. How to Combine Systems? xxxxxxxxxxxxxxxxxxxxxxxxxxxx The Monocratic Algebra Approach ------------------------------- Start from an algebra system, incorporate proving. The Monocractic Logic Approach ------------------------------- Start from a proving system, incorporate more algebra. The Monocratic Tabula Rasa Approach ------------------------------------- Design and implement a new system for all phases of mathematics including proving. The Democratic Approach -------------------------- Design and implement one interface and a high-level problem solving driver that organizes the access to many existing algebra and proving systems. How to Master Complexity and Make Proving More Efficient? XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX Special provers for particular areas In contrast: there are certain proof techniques that are general and common to many areas, even "universal" What is an area? ------------------- Classes of areas can be defined axiomatically Classes of areas can be defined by a functor that constructs a class of domains from a given class of domains The are many special and quite efficient theorem provers around for certain axiomatically defined areas Each functor should come with its prover In fact, "working in an area" could mean "invent special proving techniques for that area" Special provers should be combined in a systematic way: "proof planning" In other words: "working in an area" becomes "inventing proof techniques for combining known general and special proof techniques for the particular fields" The systems we have in mind must have the possibility of extendibility by the user A future mathematician uses "the system" in an interactive way for proving certain theorems in his area but also extends "the system" by his own proof techniques Discussion XXXXXXXXXXXXXXXXX Who is the user we address? =================== * (Blackbox) users of mathematics * Mathematicians who produce mathematics again there are two subgroups mathematicians who oppose sytems mathematicians who want to use systems "The new system": One view final goal is to offer better math software systems to all users of mathematics one subview: we need proving in order to improve the quality of our math software systems second subview: we want improved proving and for this we need algebra "The new system": Second view final goal is to offer a better system for mathematicians who produce mathematics Examples of benchmarks for the system: inner mathematical examples: e.g. write a book in one logic and software system frame (example: book on Groebner bases) real world problem solving examples: hardware verification Industry involvement: publishing company CA softwares very difficult! companies involved in software verification Meetings: July 17-20, Hagenberg in the frame of IMACS ACS one afternoon business session for our TMR October ? in Dagstuhl: writing of the proposal demo session Coupling of systems: loose coupling ? close coupling ? Or will there be one strong system that will dominate the market. hardware verification SIEMENS, Daimler, IBM ?? math training ? edu ministeries ?