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 semidecidable : 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 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?