KnowledgeBase » 
SEMINAR
» ID = 355
CADE Practice Talk
by Wilfred Z. Chen
1991-1992
This work currently is a mix of original research, philosophical reflections, and review of relevant work (such as bottom-up vs top-down + top-down a la Pollock. For the thesis, I need to flesh out these components fully; for CADE, I need to find the right balance among these different concerns.
Goals of this line of research:
- Bring all our declarative knowledge to bear on a specific problem, to a degree;
- Non-uniform reasoning controlled by lemma library;
- What is forward chaining? Why forward chaining? What are some of the advantages? Motivations for looking at forward chaining, mainly two:
- Intuitive motivation: we seem to have mechanisms to manage large number of facts and small number of conjectures; inference from facts more automatic/subconscious, resoning about conjectures more focused and conscious. One reason maintenance of facts easier than conjectures is that we often don't have to maintain the dependencies among facts, but dependencies among conjectures is all-important.
- Systematic non-repetitive generation of facts, versus potentially repetitive and circular generation of conjectures. Why don't we do the same thing with conjectures? Maintain a pool of facts and a pool of conjectures. This is a new idea that I will pursue. One reason for the way things are as they are is that facts are more worth remembering than conjectures. We quickly give up on bad conjectures, but there are no bad facts, just perhaps irrelevant facts. So perhaps we need three pools: facts, good conjectures, bad conjectures. We remember bad conjectures only to prevent them from being generated again.
- Intuitive motivation: we seem to have mechanisms to manage large number of facts and small number of conjectures; inference from facts more automatic/subconscious, resoning about conjectures more focused and conscious. One reason maintenance of facts easier than conjectures is that we often don't have to maintain the dependencies among facts, but dependencies among conjectures is all-important.
- Common theme to both game playing and mathematical reasoning: In both cases, it is desirable to replace search with knowledge. But in mathematics, use of knowledge is much more critical than in games, where search with simple heuristics can often get acceptable results. But the holy grail in both is still how to apply knowledge effectively to reduce search.