Practical partition-based theorem proving for large knowledge bases
Bill MacCartney, Sheila A. McIlraith, Eyal Amir, Tomás E. Uribe · 2003
Query answering over commonsense knowledge bases typically employs a first-order logic theorem prover. While first-order inference is intractable in general, provers can often be hand-tuned to answer queries with reasonable performance in practice.