摘要: OTTER (Organized Techniques for Theorem-proving and Effective Research) is a resolution-style theorem-proving program for first-order logic with equality. OTTER includes the inference rules binary resolution, hyperresolution, UR-r... 展开
作者 | McCune, W W | ||
---|---|---|---|
原报告号 | DE94007457 | 总页数 | 67 |
主办者 | Department of Energy, Washington, DC. | ||
报告分类号 | [72B: Mathematical Sciences: Algebra, Analysis, Geometry, & Mathematical Logic] | ||
报告类别/文献类型 | DE / NTIS科技报告 | ||
关键词 | Computer applications EDB/990200 |