The authors describe a declarative language for expert systems using natural deduction and for addressing the problem of uncertainty. The authors’ desire to develop a non-resolution theorem prover for expert systems is a useful one, allowing for more intelligent interaction between man and machine. Their first order logic (SNARK) is designed to this end, incorporating a fairly standard semantics along with a fuzzy logic for measurements of uncertainty. The syntax for rules is identical to most natural deduction systems: antecedents and a goal (or consequent). From the report, however, it is difficult to evaluate how their proof technique is different from that of the IMPLY system of Bledsoe and Tyson [1]. Furthermore, no comparison is made to other (possibly related) research (e.g., Reiter [2,3]).

Their appeal to Fuzzy Logics (FLs) is an unfortunate one. Although well suited for measurements of class membership in some cases, there are well-known problems when attempts are made to treat certainty of belief or vagueness within this framework. For example, self-contradictory predicates such as &lgr; x [ P ( x ) ∧ - P ( x ) ] is a characteristic function that should always give the value 0, which it does not in FL (e.g., it might be .5). Similarly, tautologous characteristic functions, &lgr; x [ P ( x ) ∨ - P ( x ) ] should always return the value 1, which is also not the case for FL. In conclusion, it is difficult to discern what is new in this work, due in part perhaps to their nonstandard notation and nomenclature.