Deduction and Presentation in rho Log
Deduction and Presentation in rho Log
复制标题
rho Log 中的推导和呈现
DOI：
10.1016/j.entcs.2003.12.033
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Florina Piroi
中科院分区：
文献类型：
--
作者：
M. Marin;Florina Piroi
我们描述了在数学中实现的一个基于规则的系统的演绎和证明能力。该系统可以计算证明对象，该证明对象是符合用户给出的规范的演绎的内部表示。它还可以以人类可读的格式以不同级别的细节可视化此类演绎。计算证明对象的呈现是以自然语言风格来完成的，该自然语言风格是从定理的证明呈现风格中根据我们的需要而衍生和简化的。
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.