EXPLAIN: A tool for performing abductive inference
Işıl Dillig, Thomas Dillig · 2013
Abstract. This paper describes a tool called Explain for performing abductive inference. Logical abduction is the problem of finding a simple explanatory hypothesis that explains observed facts. Specifically, given a set of premises Γ and a desired conclusion φ, abductive inference finds a simple explanation ψ such that Γ ∧ ψ | = φ, and ψ is consistent with known premises Γ. Abduction has many useful applications in verification, including inference of missing preconditions, error diagnosis, and construction of compositional proofs. This paper gives a brief tutorial introduction to Explain and describes the basic inference algorithm. 1