New techniques for inference in assumption-based truth maintenance systems
Claudette Cayrol, Michel Cayrol, OLIVIER PALMADE · 2002
Presents a new and unifying formalization of the inference techniques involved in assumption-based truth maintenance systems (ATMS). Basic concepts of ATMS are briefly reviewed. Then an original inference system, called P-deduction, is presented, which enables us to build a propositional backward-chaining prover. It is shown how to exploit the results provided by the proof algorithm in order to compute labels, interpretations, and nogoods.