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 First-OrderTheorem 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 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

Speaker notes:

Content Tools


There are currently no sources for this slide.