Mircea Marin, Florina Piroi,
"Deduction and Presentation in $\rho$Log"
, in F. Kamareddine: Proceedings of the Mathematical Knowledge Management Symposium, Serie ENTCS, Vol. 93, Elsevier, Seite(n) 161--182, 2-2004, ISBN: 044451290X
Deduction and Presentation in $\rho$Log
Sprache des Titels:
Proceedings of the Mathematical Knowledge Management Symposium
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.