Abduction as Satisfiability

Abstract. Abduction is reasoning in propositional or first-order logic that provides explanations for observations. We show how context-free parsing and automated planning can be formulated using abductive rules and present a fast prover based on propositional satisfiability. Further-more we show how weighted abduction can be efficiently implemented in the prover