A logically complete reasoning maintenance system based on a logical contraint solver.

*(English)*Zbl 0747.68072
Artificial intelligence, IJCAI-91, Proc. 12th Int. Conf., Sydney/Australia 1991, 295-299 (1991).

[For the entire collection see Zbl 0741.68016.]

The paper describes an original assumption-based truth maintenance system (ATMS) that is logically complete. The power of the system comes from the properties of the canonical representation of propositional formulas by typed decision graphs. Typed decision graphs are amongst the most compact representations of Boolean functions, and have been successfully used to formal verification of digital circuits and VLSI circuit design. The reasoning maintenance system, integrated into the proposed ATMS, and based on the mentioned representation, is implemented in the \(C\) language and contains an incremental garbage collector that guarantees that the memory use is kept minimal during execution. This ATMS was integrated in the prototype version of a complex blast furnace computer aided piloting system.

The paper describes an original assumption-based truth maintenance system (ATMS) that is logically complete. The power of the system comes from the properties of the canonical representation of propositional formulas by typed decision graphs. Typed decision graphs are amongst the most compact representations of Boolean functions, and have been successfully used to formal verification of digital circuits and VLSI circuit design. The reasoning maintenance system, integrated into the proposed ATMS, and based on the mentioned representation, is implemented in the \(C\) language and contains an incremental garbage collector that guarantees that the memory use is kept minimal during execution. This ATMS was integrated in the prototype version of a complex blast furnace computer aided piloting system.

Reviewer: N.Curteanu (Iaşi)