In this paper, we describe our preliminary justification techniques for the transactional queries executed in the tabled Horn Transaction Logic. Transaction Logic is an extension of classical logic programming with state updates similar to database transactions suitable for tasks ranging from processing complex event workflows to AI planning. Execution with tabling is a technique to cache the calls, callstates and answers in a searchable structure, so that the same call in the same state is not re-executed ad-infinitum and the computation is guaranteed to terminate for the Transaction Datalog. The justification or truth maintenance is the process of constructing evidence for the answers derived by tabled evaluation. The tabled execution entailment does not support easy extraction of the justification due to the construction of the derivation tree with results from various parts of the call-answer table. We extract the justification using pointers from the call-answer table to nodes of the derivation tree and additional evidence constructed from the execution trail.
展开▼
