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.

Completeness & Decidability (2)

  • FOL is only semi-decidable : If a conclusion follows from premises, then a complete proof system (like resolution) will find a proof.

    • If there’s a proof, we’ll halt with it (eventually)

    • However, If there is no proof (i.e. a statement does not follow from a set of premises), the attempt to prove it may never halt

  • From a practical point of view this is problematic

    • We cannot distinguish between the non-existence 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?


Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.