STeP's automatic first-order validity checker

This page contains information on STeP's automatic first-order prover, which combines unification-based first-order reasoning and ground decision procedures. It supplements the paper

Nikolaj Bjørner, Mark Stickel and Tomás E. Uribe. A practical integration of first-order reasoning and decision procedures. In Proc. of the 14'th International conference on Automated Deduction CADE-14, pp. 101-115, Springer-Verlag, vol. 1249 of LNCS. Townsville, Australia, July 1997.

Examples

• The Philips Protocol
• The Railroad crossing example
• Simple structure sharing
• The SRT division table
• Examples entered by guests
• Try it your self

Links

Nikolaj Bjørner's home page

Tomás E. Uribe's home page

Mark Stickel's home page