Executable temporal logic for non-monotonic reasoning (Q679335)

Nonmonotonic reasoning is the main topic of the paper. The reasoning is viewed as a (kind of) process. An approach to specifying, reasoning about, and executing processes is applied in this paper to nonmonotonic reasoning. The formalism of temporal logic is used to specify and verify processes in general. If a class of processes can be specified by a form of temporal logic which can be executed, then a general execution mechanism for this class is available. In the paper a class of nonmonotonic reasoning processes is studied. The processes are described semantically by reasoning traces they produce. The traces are viewed as temporal models. They can be specified by temporal rules. It is shown in the paper that a fragment of infinitary temporal epistemic logic is suitable for describing any set of traces. It is shown that it is possible to execute finite specifications in the language of temporal epistemic logic. An algorithm which can execute any specification of reasoning is given in the paper for the case when the signature is finite. Although the execution of temporal rules is similar to existing executable temporal logics, the consistency checks are treated differently. They are treated as declarative tests in the future, not as imperative commands for the future. A criterion of correct executions (for the finite signature) is stated in the paper. For a finite theory of reasoning the algorithm can construct precisely its minimal models. A study of sceptical and credulous entailment is possible in this framework. When the consistency checks are not allowed, the induced reasoning process is monotonic. If we use heuristic knowledge to guide the reasoning process, we can make the algorithm more efficient.