Otter: An Automated Deduction System
2007-05-08 17:53
260 查看
Contents
DescriptionComputational Environment
Availability Version 3.3
Documentation
Example Inputs and Outputs
Accomplishments
Performance on the TPTP Problems
Bugs and Fixes
Mailing Lists
Copyrights and License
Related Pages
Try Otter right now with Son of BirdBrainA sample Otter proof
New Results obtained with Otter and related programs
Mace searches for small models
EQP, a prover for equational logic with associative unification
Automated Reasoning at Argonne
External Work
Some of the Otter and Mace usersDescription
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.Currently, the main application of Otter is research in abstract algebra and formal logic. Otter and its predecessors have been used to answer many open questions in the areas of finite semigroups, ternary Boolean algebra, logic calculi, combinatory logic, group theory, lattice theory, and algebraic geometry.
Computational Environment
Otter is coded in ANSI C and is portable, easy to install, and fast. It has been used mostly on Unix-like systems, but limited versions also run in Microsoft Windows.Availability
The current version is Otter 3.3, and the distribution package includes Mace 2.2.Download Otter 3.3 / Mace 2.2.
Documentation
The Otter distribution package contains all source code, installation instructions, users guides in PDF and PostScript formats, and a collection of test problems.Otter 3.3 Reference Manual
Several books on Otter and its applications are available.
Automated Reasoning and the Discovery of Missing and Elegant Proofs, by L. Wos and G. W. Pieper, Rinton Press (2003).
Automated Reasoning with Otter, by J. A. Kalman, Rinton Press (2001).
A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning , by Larry Wos, with Gail Pieper, World Scientific (2000).
Automated Deduction in Equational Logic and Cubic Curves, by W. McCune and R. Padmanabhan, Springer-Verlag LNCS #1095 (1996).
The Automation of Reasoning: An Experimenter's Notebook with Otter Tutorial, by Larry Wos, Academic Press (1996).
Automated Development of Fundamental Mathematical Theories, by Art Quaife, Kluwer Acadamic Publishers (1992).
Example Inputs and Outputs
Here are the test problems from the distribution package.Otter 3.3 test problems.
Mace 2.2 test problems.
Accomplishments
See the New Results Page (way out of date) for a summary of new results that have been obtained with Otter and other Argonne deduction programs.Performance on the TPTP Problems
TPTP is a large problem set for testing first-order automated theorem-proving programs. Otter has been run on all of the TPTP problems, and the following results are available.Otter 3.1 and MACE 1.4 on TPTP v2.3.0 (table created May 22, 2000).
Bugs and Fixes
See the Change-log File.These changes have been made in the development version of Otter. We don't retain the source code for the intermediate versions (e.g., Otter-3.2d).
If you need any of these changes, we can give you a snapshot of the current version (source code), which should contain all of the updates listed in the Change-log (and then some).
Mailing Lists
The mailing listsotter-announce
otter-help
otter-development
have been discontinued.
Copyrights and License
See the Otter/MACE Legal Page. These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.相关文章推荐
- C++ Coding Standards Item 2 : Use an automated build system
- An algorithm for routing control of a tandem automated guided vehicle system
- 系统启动时出现 An error occurred during the file system check.
- 无法在Web服务器上启动调试."System.Net.DigestClient"的类型初始值设定项引发异常,Unable to debug System.Net.DigestClient throws an exception
- This is an example of state transitions - for Transition System Semantics of DFL as a Scientific Workflow Language
- Effective GUI Test Automation: Developing an Automated GUI Testing Tool
- linux系统启动报错:An error occurred during the file system check(linux学习记录)
- 解决Set property 'System.Windows.ResourceDictionary.DeferrableContent'threw an exception.
- System.Net.WebException : The remote server returned an error: (415) UNSUPPORTED MEDIA TYPE
- System.Net.Sockets.SocketException: An address incompatible with the requested protocol was used.
- 'Set property 'System.Windows.ResourceDictionary.DeferrableContent' threw an exception.
- 突然断电,出现'an error occurred during the file system check'错误解决办法
- Differences Between a BI/Data Warehouse System and an OLTP System
- 在使用jetty配置jndi的时候报错“Need to specify class name in environment or system property, or as an applet pa
- The type 'System.Data.Objects.DataClasses.EntityObject' is defined in an assembly that is not refere
- Windows Streams - An Introduction to File System Streams
- System.AccessViolationException: Attempted to read or write protected memory. This is often an indication that other memory is corrupt".
- System.Configuration.ConfigurationErrorsException: An error occurred creating the configuration sect
- What is an entity system framework for game development?
- linux出现an error occurred during the file system check