摘要：本文提出了相干命题逻辑系统R的一种演绎生成算法——试探法。该算法采用后向推理法，依据推理规则将待证命题逐步分解成子命题并构造一棵证明树，对系统R中的定理证明取得了较好的效果。

关键词：相干逻辑 自动推理 演绎 可读证明 证明树 

单位：华东师范大学软件学院 上海200062