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.

Theorem Proving Summary

  • Resolution is a sound and complete inference procedure for First-Order Logic

  • Due to its complexity and remaining limitations FOL is often not suitable for practical applications

  • Often formalisms expressivity and complexity results are more appropriate:

    • Description Logics

    • Logic Programming


Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.