OlliG
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.
Limitations of FirstOrderTheorem Proving
 From a practical point of view this is problematic
 We cannot distinguish between the nonexistence of a proof or the failure of an implementation to simply find a proof in reasonable time.
 Theoretical completeness of an inference procedure does not make a difference in this cases

Does a proof simply take too long or will the computation never halt anyway?

Due to its complexity and remaining limitations FOL is often not suitable for practical applications
 Often less expressive (but decideable) formalisms or formalisms with different expressivity are more suitable:
 Description Logics

Logic Programming
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.