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
Tools
Sources (0)
Tags (0)
Comments (0)
History
Usage
Questions (0)
Playlists (0)
Quality
Sources
There are currently no sources for this slide.