Current Slide

Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.

Concrete System: Prover9

  • First-Order theorem prover
    • Homepage: http://www.cs.unm.edu/~mccune/prover9/
    • Successor of the well known “Otter” theorem prover
    • Under active development, available for several platforms and released under the GPL
    • Graphical user-interface and extensive documentation make Prover 9 comparatively user friendly
  • Core of system builds on resolution / paramodulation as inference method
  • Prover9 works in parallel with external component „Mace4“
    • Mace4 searches for finite models and counterexamples
    • This helps to avoid wasting time searching for a proof by first finding a counterexample

Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.