hdm
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[hdm] notes from last wednesday's phone conversation


From: Joe Corneli
Subject: [hdm] notes from last wednesday's phone conversation
Date: Sun, 26 Mar 2006 22:35:26 -0500 (EST)

Last week during our phone conversation I put together a big bubble
diagram (a sort of low-tech sonoluminescene?).  One of these days
maybe I'll have a scanner and I can send such things to you easily.
One of these years maybe I'll have an bubble-recognizing program and I
can send the code for such things to you easily.  But that time is not
now, so I will simply redact it (at least in part) as a loose
hetrarchy.

legality
 doing what mathematicians do
 
parsing
 hcode
  apmxi
  100 example definitions (HDMp3)
  processing formulas vs processing NL
  lisp-like or lisp-based
 query answering
 formal
  some precedent in HOL &c.
  possibly better precedent in the work of Don Simon (see wiki)
  we should come up with some complete examples
   pick some Schuam's books and work with those?
 informal
  monadology
   frames
  data management

understandability
 linguistics
 formal checking
 thinking the way people do
  (sometimes intermingling with thinking the way machines do)

how might some examples be expressed
 definitions
 proofs
 theorems
 code
 proof-check

what does it mean to check a proof?
 math representation language (MRL)/coherent notation
  principles
   names
   functions
   bound variables
  distinct from informal frame-based language

value/reality check
 teaching
 making money
 being useful in research
 checking proofs
 intelligent search/organization
 personalized tutoring

knowledge requirements
 know what words mean
 know what proof ideas are
 establish common "symbols"
  (here, think of proof ideas as represented as symbols)

inference rules
 must be able to represent them
 must know what they are
 allow any valid rule (when are rules valid?)
 uses a syntax similar to the 3 principles of MRL (?)

metatheorems
 valid rules
 rules that aren't going to be in a book on the subject
 intuitian
 formal (i.e., based on form)

eventual goals for usefulness
 in robotics
 in economics
 in AI generally




reply via email to

[Prev in Thread] Current Thread [Next in Thread]