Modality and interrupts (Q1891265)

Conventional declarative systems are inappropriate for use in real time or other systems that provide only limited computational resources because of the unpredictable amount of time needed for them to respond to queries. With the purpose of to get over these difficulties the declarative language Prolog is expanded by the modal operator of necessity, serving in terms of anytime reasoning to indicate the mark points (it is the points of negation) at which inference can be interrupted and an approximate answer computed and returned. The latter is computed quickly and can be gradually refined if time permits. A truth functional semantics over distributive bilattices is used for modality, not the Kripke's possible worlds semantics. The modal system \(S5\) comes out in the simplest case of four truth values only. A distributive bilattice is a sextuple \((B, \wedge, \vee, \cdot, +, \neg)\) such that 1) \(B\) is the finite nonempty set of truth values; 2) \((B, \wedge, \vee)\) and \((B, \cdot, +)\) are both complete lattices; 3) \(\neg \) is a mapping \(B \to B\) such that \(\neg \neg A = A\) and \(\neg\) is a lattice homomorphism from \((B, \wedge, \vee)\) to \((B, \vee, \wedge)\) and from \((B, \cdot, +)\) to itself; 4) each of the bilattice operation distributes with respect to the others, so that \(x \wedge (y + z) = x \wedge y + x \wedge z\) and so on. A truth assignement is a function \(\varphi : L \to B\), where \(L\) is the set of Prolog's clauses (with modality), such that if \(\varphi\) labels both \(q\) and \(q \to r\) as true, then \(r\) is labeled as true too. The method of truth assignment is sufficiently powerful to describe nonmonotonic reasoning based on autoepistemic logic. Prolog's negation-as-failure operator, and Kripke-style possible worlds semantics.