Description |
This work stems on [41], [42] and is related to diagnosis where observed symptoms have to be explained by faults. The previously existing proposals are ad hoc or, as in [43], [59], they are too close to standard logic in order to make a satisfactory diagnosis. Our proposal starts from propositional logic and introduces new causal formulas, built on causal atoms such as ($ \alpha$ causes $ \beta$) intended to mean: “$ \alpha$ causes $ \beta$”. There are also “ontological atoms” such as ($ \alpha$ IS_A $ \beta$) (roughly $ \alpha$ is of kind $ \beta$). We have provided a set of inference rules [7] stating where $ \beta$ can be explained by some $ \alpha$. These explanations are formalized by explanation atoms of the kind ($ \alpha$ explains $ \beta$ if_possible Im1 ${{\#947 _1,\#8943 ,\#947 _n}}$): when all the $ \gamma$i\'s are possible together in the context of the given data, then $ \alpha$ explains $ \beta$. The simplest generating rule states that if ($ \alpha$ causes $ \beta$) then ($ \alpha$ explains $ \beta$ if_possible {$ \alpha$}). This is the simplest set of “conditions” in the formalism. It is worth noting that the rules state also that if ($ \alpha$ causes $ \beta$) then $ \alpha$$ \rightarrow$$ \beta$, thus in fact here “if_possible {$ \alpha$}” is equivalent to “if_possible {$ \alpha$, $ \beta$}”. Despite this rule, the connexions between causes and $ \rightarrow$ are rather loose. These connexions are a known difficulty in causal formalisms. Our solution limits the number of connexions between these two operators, while keeping the formalism simple and natural enough. One of the rules states that if ($ \alpha$ causes $ \beta$) and ($ \beta$i IS_A $ \beta$) then ($ \alpha$ explains $ \beta$i if_possible {$ \alpha$, $ \beta$i}). This is the way to deal with alternative effects. The use of an elementary ontology makes the formalism easy to use, making a clear separation between three kinds of data: ordinary, causal and ontological.
In order to test the theory with toy-like examples we have translated our causal formalism into DLV [68], an Answer Set Programming implementation. Answer Set Programming [38] is a recent evolution of logic programming, where a “program” is a set of rules close to logical formulas, and the “result” is a set of some kinds of models of these formulas. The present implementations of this declarative formalism are rather efficient. This translation was relatively easy, even if some little improvements in the existing implementations could help the task of the programmer [15].
We intend to test more examples, and to adapt the theory if some unwanted behavior still remains. The translation into ASP is of great help, since the rules in ASP reflect directly the rules of the formalism, so it is easy to test any modification of the theory.
Notice that the problems encountered by workers on diagnosis have been one of the main motivations for introducing default reasoning (reasoning in the “normal course of events”, thus allowing exceptions) and that an important part of the presently active work on causation is an illustration of this long lasting close relationship.
We have continued our work on one of the leading default formalism: circumscription. The idea of circumscription is to deal with the problem of default reasoning as follows. A “rule by default” (R) “if $ \alpha$ then $ \beta$” will be transformed into the rule “if $ \alpha$ and ¬exceptionR then $ \\beta$”. Circumscription will keep the exceptions to the minimum possible. Recently, a new method of computation has been proposed [66], where the old logical notion of forgetting propositional symbols (or reducing the logical vocabulary, already studied by Boole) has been generalized to the notion of forgetting literals, and this was shown to allow tractable computation of some kinds of circumscription. We have extended this notion by allowing some propositional symbols to vary while forgetting literals, in order to deal with the really useful kinds of circumscription. Our new results [5] consist in a formal study of the connexions of this notion with already known formalisms, and in an extensive description of a constructive method for computing this notion of literal forgetting. This is important since it improves significantly previously known results ([76], [86], [66]) applying this kind of method to the computation of circumscription or other default formalisms. |