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.
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
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?
This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License