ATP
Software Description
ATP is a lisp implementation of a model elimination theorem prover
for full first order logic as well as context logic. This is a small, but
fairly efficient theorem prover based on Stickel's PTTP (prolog technology
theorem prover) method. It should be easy to extend and easy to embed in
a larger application.
Reference Manual
- ATP Reference Manual.
Software Availability
- ATP is not being distributed at this time.
Problems or Information?
- Contact
Last modified: Tuesday, 22-Jan-2008 22:22:54 PST