We describe the deductive and proof presentation capabilities of a rule-based system implemented in Mathematica. The system can compute proof objects, which are internal representations of deduction derivations which respect a specification given by the user. It can also visualize such deductions in human readable format, at various levels of detail. The presentation of the computed proof objects is done in a natural-language style which is derived and simplified for our needs from the proof presentation styles of Theorema.
| Original language | English |
|---|
| Title of host publication | Proceedings of the Mathematical Knowledge Management Symposium |
|---|
| Editors | F. Kamareddine |
|---|
| Publisher | Elsevier |
|---|
| Pages | 161-182 |
|---|
| Number of pages | 22 |
|---|
| Volume | 93 |
|---|
| ISBN (Print) | 044451290X |
|---|
| Publication status | Published - Feb 2004 |
|---|
- 101 Mathematics
- 101001 Algebra
- 101005 Computer algebra
- 101009 Geometry
- 101012 Combinatorics
- 101013 Mathematical logic
- 101020 Technical mathematics