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?
