Otter is, contrary to expections, not a furry water dwelling animal beloved of children, but an "automated deduction system ... designed to prove theorems stated in first-order logic with equality". Logic is fairly well defined (isn't it? Correct me if I'm wrong); I wonder whether Otter works by simply traversing and closing down logic branches, or whether there's much more to it, optimisations and otherwise. It's at times like this I wish I had formal training in all this stuff.
Otter is, contrary to expections, not a furry water dwelling animal beloved of children, but an "automated deduction system ... designed to prove theorems stated in first-order logic with equality". Logic is fairly well defined (isn't it? Correct me if I'm wrong); I wonder whether Otter works by simply traversing and closing down logic branches, or whether there's much more to it, optimisations and otherwise. It's at times like this I wish I had formal training in all this stuff.