EXPLAIN: A tool for performing abductive inference

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. © 2013 Springer-Verlag.