|
|
| 项目描述: |
Our current automated deduction system Otter is designed to prove theorems stated in first-order logic with equality. Otter's inference rules are based on resolution and paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting, and strategies for directing and restricting searches for proofs. Otter can also be used as a symbolic calculator and has an embedded equational programming system. Otter is a fourth-generation Argonne National Laboratory deduction system whose ancestors (dating from the early 1960s) include the TP series, NIUTP, AURA, and ITP.
本软件用于抽象代数，符号演算，形式逻辑研究方面的专业软件。 |
| 类别: |
| |
|
发布者：
uhml
|
|
| 最新发布源码包 |
|
没有发布任何的软件包! |
|
form Handler - 项目摘要