Knowledge Assimilation and Proof Restoration through the Addition of Goals

Normal proof procedures in abductive logic programming assume that a given program does not change until the proof is completed. However, while a proof is being constructed, new knowledge which affects the proof might be acquired. This paper addresses two important issues: 1. How is it confirmed that the proof being constructed is not affected by the addition of a clause? 2. If affected, how are the invalid parts of the proof restored? The abductive proof procedure used in this paper is Kakas and Mancarella's procedure and is extended to prepare for proof checking and proof restoration. It is shown that any invalid part of a proof can be restored if some additional goals are solved. These additional goals can be added before a proof is completed.