A logically complete reasoning maintenance system based on a logical contraint solver. (English) Zbl 0747.68072

Madre, J. C.; Coudert, O.

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.

Reviewer: N.Curteanu (Iaşi)

MSC:

68T20	Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T27	Logic in artificial intelligence
68T35	Theory of languages and software systems (knowledge-based systems, expert systems, etc.) for artificial intelligence

Keywords:

reasoning maintenance system; logically complete ATMS; Typed decision graphs

Citations:

Zbl 0741.68016