Premium
Using crucial literals to select better theories
Author(s) -
SATTAR ABDUL,
GOEBEL RandY
Publication year - 1991
Publication title -
computational intelligence
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.353
H-Index - 52
eISSN - 1467-8640
pISSN - 0824-7935
DOI - 10.1111/j.1467-8640.1991.tb00331.x
Subject(s) - literal (mathematical logic) , extension (predicate logic) , falsifiability , computer science , truth value , set (abstract data type) , constraint (computer aided design) , artificial intelligence , mathematics , epistemology , algorithm , philosophy , programming language , geometry
When Horn clause theories are combined with integrity constraints to produce potentially refutable theories, Seki and Takeuchi have shown how crucial literals can be used to discriminate two mutually incompatible theories. A literal is crucial with respect to two theories if only one of the two theories supports the derivation of that literal. In other words, actually determining the truth value of the crucial literal will refute one of the two incompatible theories. This paper presents an integration of the idea of crucial literal with Theorist, a logic‐based system for hypothetical reasoning. Theorist is a goal‐directed nonmonotonic reasoning system that classifies logical formulas as possible hypotheses, facts, and observations. As Theorist uses full clausal logic, it does not require Seki and Takeuchi's notion of integrity constraint to define refutable theories. In attempting to deduce observation sentences, Theorist identifies instances of possible hypotheses as nomological explanations: consistent sets of hypothesis instances required to deduce observations. As multiple and mutually incompatible explanations are possible, the notion of crucial literal provides the basis for proposing experiments that distinguish competing explanations. We attempt to make three contributions. First, we adapt Seki and Takeuchi's method for Theorist. To do so, we incrementally use crucial literals as experiments, whose results are used to reduce the total number of explanations generated for a given set of observations. Next, we specify an extension which incrementally constructs a table of all possible crucial literals for any pair of theories. This extension is more efficient and provides the user with greater opportunity to conduct experiments to eliminate falsifiable theories. A prototype is implemented in CProlog, and several examples of diagnosis are considered to show its empirical efficiency. Finally, we point out that assumption‐based truth maintenance systems (ATMS), as used in the multiple fault diagnosis system of de Kleer and Williams, are interesting special cases of this more general method of distinguishing explanatory theories.