math discovery

Gerry Wolff gerry at sees.bangor.ac.uk
Fri Jun 18 02:44:23 PDT 1999


Chuck Carlson wrote:
> 
> Hello all,
> 
> Does anyone have any comment or know of resources regarding automated
> math discovery
> involving the principles of compression and/or entropy?
> 
> I know about Douglas Lenat's AM program but that started with a
> knowledge of sets
> and used lots of heuristics.
> 
> I'd like to use genetic algorithms with a fitness function involving
> compression or
> entropy to evolve structures that would probably start out representing
> simple maths
> like addition and subtraction.
> 
> Thanks,
> 
> Chuck Carlson

I've done a search in the Science Citation Index for the years 1981-1999
using the search pattern math* & (induc* OR discover* OR learn*) but the
results are a bit disappointing. One difficulty is that 'mathematical
induction' has a meaning which is different from the induction of
mathematical functions.

I know that H Simon has worked in this area (one reference in the list
below) and Pat Langley edited a book on it some time ago but I can't
find the details.

A selection of the most relevant of the search results is below.

Gerry

-----------

(1)   TI: Parallel processing and OOP as an analogy for the discovery of 
          certain mathematical proofs
      AU: Hennefeld_J
      NA: CUNY BROOKLYN COLL,DEPT MATH,BROOKLYN,NY,11210
      JN: COMPUTERS & MATHEMATICS WITH APPLICATIONS, 1997, Vol.33, No.6, 
          pp.91-97
      IS: 0898-1221
      DT: Article
      AB: This paper presents a heuristic methodology that can be used
to
          discover (and/or better understand) proofs of some
mathematical
          theorems, when the statement of the theorem involves a set for 
          which every element should be ''processed.'' This heuristic, 
          which has a number of interesting connections with recent 
          trends in computer program design, is called the Method of 
          Uniform Parallel Object-Modules, after the concepts of 
          modularization, parallel processing, and object oriented 
          programming.
      WA: heuristic, object-oriented, parallel processing, proof

(2)   TI: A computational approach to George Boole's discovery of 
          Mathematical Logic
      AU: deLedesma_L, Perez_A, Borrajo_D, Laita_LM
      NA: UNIV POLITECN MADRID,FAC INFORMAT,BOADILLA MONTE 
          28660,MADRID,SPAIN
          UNIV CARLOS III MADRID,ESCUELA POLITECN SUPER,LEGANES 
          28911,MADRID,SPAIN
      JN: ARTIFICIAL INTELLIGENCE, 1997, Vol.91, No.2, pp.281-307
      IS: 0004-3702
      DT: Article
      AB: This paper reports a computational model of Boole's discovery 
          of Logic as a part of Mathematics. George Boole (1815-1864) 
          found that the symbols of Logic behaved as algebraic symbols, 
          and he then rebuilt the whole contemporary theory of Logic by 
          the use of methods such as the solution of algebraic
equations.
          Study of the different historical factors that influenced this 
          achievement has served as background for our two main 
          contributions: a computational representation of Boole's Logic 
          before it was mathematized; and a production system, BOOLE2, 
          that rediscovers Logic as a science that behaves exactly as a 
          branch of Mathematics, and that thus validates to some extent 
          the historical explanation. The system's discovery methods are 
          found to be general enough to handle three other cases: two 
          versions of a Geometry due to a contemporary of Boole, and a 
          small subset of the Differential Calculus. (C) 1997 Published 
          by Elsevier Science B.V.
      KP: HEURISTICS

(3)   TI: Analyzing mathematical models with inductive learning networks
      AU: Steiger_DM, Sharda_R
      NA: UNIV N CAROLINA,DEPT INFORMAT SYST & OPERAT 
          MANAGEMENT,GREENSBORO,NC,27412
          OKLAHOMA STATE UNIV,DEPT MANAGEMENT,STILLWATER,OK,74078
      JN: EUROPEAN JOURNAL OF OPERATIONAL RESEARCH, 1996, Vol.93, No.2, 
          pp.387-401
      IS: 0377-2217
      DT: Article
      AB: After building and validating a mathematical model, the 
          decision maker frequently solves (often many times) a slightly 
          different version of the model. That is, by changing various 
          input parameters and re-running different model instances, he 
          tries to develop insight(s) into the workings and tradeoffs of 
          the complex system represented by the model. However, very 
          little research has been devoted to helping the decision maker 
          in this important model analysis endeavor. This paper 
          investigates the application of two inductive learning 
          technologies, backpropagation neural networks and the group 
          method of data handling, to the analysis of multiple instances 
          of a mathematical model. Specifically, these two techniques
are
          compared in the analysis tasks of identifying key factors and 
          determining key relations between uncertain and/or unknown 
          model parameters and the associated objective function values.
      KP: SENSITIVITY ANALYSIS, NEURAL NETWORK, OPTIMIZATION, OUTPUT
      WA: neural networks, group method of data handling (GMDH), 
          inductive learning networks, model analysis, decision support 
          systems

(4)   TI: Automated mathematical induction
      AU: Bouhoula_A, Kounalis_E, Rusinowitch_M
      NA: INRIA LORRAINE,F-54600 VILLERS LES NANCY,FRANCE
          CRIN,F-54600 VILLERS LES NANCY,FRANCE
          LAB INFORMAT I3S,F-06560 VALBONNE,FRANCE
      JN: JOURNAL OF LOGIC AND COMPUTATION, 1995, Vol.5, No.5,
pp.631-668
      IS: 0955-792X
      DT: Article
      AB: Proofs by induction are important in many computer science and 
          artificial intelligence applications, in particular, in
program
          verification and specification systems. We present a new
method
          to prove (and disprove) automatically inductive properties. 
          Given a set of axioms, a well-suited induction scheme is 
          constructed automatically. We call such an induction scheme a 
          test set. Then, for proving a property, we just instantiate it 
          with terms from the test set and apply pure algebraic 
          simplification to the result. This method needs no completion 
          and explicit induction. However it retains their positive 
          features, namely, the completeness of the former and the 
          robustness of the latter. It has been implemented in the 
          theorem-prover SPIKE.
      KP: TEST SETS, TERMINATION, PROOF
      WA: theorem proving, mathematical induction, term rewriting
systems

(5)   TI: Automated mathematical induction - Preface
      AU: Zhang_H
      NA: UNIV IOWA,IOWA CITY,IA,52242
      JN: JOURNAL OF AUTOMATED REASONING, 1996, Vol.16, No.1-2, p.1
      IS: 0168-7433
      DT: Editorial

(6)   TI: Building intelligent alarm systems by combining mathematical 
          models and inductive machine learning techniques
      AU: Muller_B, Hasman_A, Blom_JA
      NA: EINDHOVEN UNIV TECHNOL,DEPT MED ELECT ENGN,POB 513,5600 MB 
          EINDHOVEN,NETHERLANDS
          MAASTRICHT UNIV,DEPT MED INFORMAT,6200 MD 
          MAASTRICHT,NETHERLANDS
      JN: INTERNATIONAL JOURNAL OF BIO-MEDICAL COMPUTING, 1996, Vol.41, 
          No.2, pp.107-124
      IS: 0020-7101
      DT: Article
      AB: In this article a technique is described to develop knowledge-
          based alarm systems for ventilator therapy, using mathematical 
          modeling and machine learning. With a mathematical model
airway
          pressure, expiratory gas flow and CO2 concentration at the 
          endotracheal tube are simulated for patients, undergoing 
          volume-controlled ventilation with constant ventilator 
          settings, during normal functioning of the breathing circuit 
          and during breathing circuit mishaps (leaks and obstructions). 
          Simulations were performed for 94 physiologically different 
          'patients', by varying airway resistance and lung/thorax 
          compliance values in the model. Each simulated breath was 
          described by a set of derived signal features and a label that 
          constituted during which event (normal function or mishap) the 
          breath was recorded. With an inductive machine learning 
          algorithm rules, linking signal feature values to breathing 
          circuit events, were created from data of 54 of the simulated 
          patients. The resulting set of rules was able to classify 99% 
          of events in the data of the remaining 40 patients correctly. 
          Of signals, measured at a ventilated lung simulator, 100% of 
          events were classified correctly.
      KP: ALGORITHM
      WA: anesthesia, inductive machine learning, intelligent alarm 
          systems, mathematical modeling, mechanical ventilation, 
          respiratory mechanics

(7)   TI: TOWARDS A MATHEMATICAL-THEORY OF MACHINE DISCOVERY FROM FACTS
      AU: MUKOUCHI_Y, ARIKAWA_S
      NA: KYUSHU UNIV 33,FUNDAMENTAL INFORMAT SCI RES INST,FUKUOKA 
          812,JAPAN
      JN: THEORETICAL COMPUTER SCIENCE, 1995, Vol.137, No.1, pp.53-84
      IS: 0304-3975
      DT: Article
      AB: This paper intends to give a theoretical foundation of machine 
          discovery from facts. We point out that the essence of a 
          computational logic of scientific discovery or a logic of 
          machine discovery is the refutability of the entire spaces of 
          hypotheses. We discuss this issue in the framework of
inductive
          inference of length-bounded elementary formal systems (EFSs), 
          which are a kind of logic programs over strings of characters 
          and correspond to context-sensitive grammars in Chomsky 
          hierarchy.
          First we present some characterization theorems on inductive 
          inference machines that can refute hypothesis spaces. Then we 
          show differences between our inductive inference and some
other
          related inferences such as in the criteria of reliable 
          identification, finite identification and identification in
the
          limit. Finally we show that for any n, the class, i.e. 
          hypothesis space, of length-bounded EFSs with at most n axioms 
          is inferable in our sense, that is, the class is refutable by
a
          consistently working inductive inference machine. This means 
          that sufficiently large hypothesis spaces are identifiable and 
          refutable.
      KP: INDUCTIVE INFERENCE, IDENTIFICATION

(8)   TI: ON THE DISCOVERY OF MATHEMATICAL CONCEPTS
      AU: EPSTEIN_SL
      NA: CUNY HUNTER COLL,DEPT COMP SCI,695 PK AVE,NEW YORK,NY,10021
      JN: INTERNATIONAL JOURNAL OF INTELLIGENT SYSTEMS, 1988, Vol.3, 
          No.2, pp.167-178
      IS: 0884-8173
      DT: Article

(9)   TI: A COMPUTER-INSPIRED MATHEMATICAL DISCOVERY
      AU: FREITAG_HT
      NA: HOLLINS COLL,MATH,HOLLINS COLL,VA,24020
      JN: ABACUS-NEW YORK, 1985, Vol.2, No.4, p.36 et seq.
      IS: 0724-6722
      DT: Article

(10)  TI: COMPUTER MODELING OF SCIENTIFIC AND MATHEMATICAL DISCOVERY 
          PROCESSES
      AU: SIMON_HA
      NA: CARNEGIE MELLON UNIV,DEPT PSYCHOL,PITTSBURGH,PA,15213
      JN: BULLETIN OF THE AMERICAN MATHEMATICAL SOCIETY, 1984, Vol.11, 
          No.2, pp.247-262
      IS: 0273-0979
      DT: Article

(11)  TI: MATHEMATICAL INDUCTION - A COMPUTER APPROACH
      AU: AUSTIN_AK
      NA: UNIV SHEFFIELD,DEPT PURE MATH,SHEFFIELD S10 2TN,S 
          YORKSHIRE,ENGLAND
      JN: MATHEMATICAL GAZETTE, 1984, Vol.68, No.443, pp.46-48
      IS: 0025-5572
      DT: Note



More information about the Casc mailing list