OlliG
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.
Limitations of FirstOrderTheorem Proving
 Entailment: KB ⊧ Q
 Entailment is a relation that is concerned with the semantics of statements

Q is entailed by KB (a set of premises or assumptions) if and only if there is no logically possible world in which Q is false while all the premises in KB are true
 Entailment for 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
Speaker notes:
Content Tools
Tools
Sources (0)
Tags (0)
Comments (0)
History
Usage
Questions (0)
Playlists (0)
Quality
Sources
There are currently no sources for this slide.