[Top][All Lists]
[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
- [hdm] notes from last wednesday's phone conversation,
Joe Corneli <=