An inference channel exists if it is possible for a low-clearance user to infer high-classification data from low-classification data. Inference channels can be blocked by upgrading the security classification of some of the low-level data. The task of eliminating inference channels is formulated for solution by the Davis-Putnam theorem-proving procedure. The procedure is augmented to search for solutions with minimum total upgrade cost.>

Multilevel relational database systems store information at different security classifications. An inference problem exists if it is possible for a user with a low-level clearance to draw conclusions about information at higher classifications. The authors are developing DISSECT, a tool for analyzing multilevel relational database schemas to assist in the detection and elimination of inference problems. A translation is defined from schemas to an equivalent graph representation, which can be presented graphically in DISSECT. The initial focus is on detection of inference problems that depend only on information all of which is stored in the database. In particular, potential inference problems are identified as different sequences of foreign key relationships that connect the same entities. Inferences can be blocked by upgrading the security classification of some of foreign key relationships. A global optimization approach to upgrading is suggested to block a set of inference problems that allows upgrade costs to be considered, and supports security categories as well as levels.>

Abduction is inference to the best explanation. In the TACITUS project at SRI we have developed an approach to abductive inference, called “weighted abduction”, that has resulted in a significant simplification of how the problem of interpreting texts is conceptualized. The interpretation of a text is the minimal explanation of why the text would be true. More precisely, to interpret a text, one must prove the logical form of the text from what is already mutually known, allowing for coercions, merging redundancies where possible, and making assumptions where necessary. It is shown how such “local pragmatics” problems as reference resolution, the interpretation of compound nominals, the resolution of syntactic ambiguity and metonymy, and schema recognition can be solved in this manner. Moreover, this approach of “interpretation as abduction” can be combined with the older view of “parsing as deduction” to produce an elegant and thorough integration of syntax, semantics, and pragmatics, one that spans the range of linguistic phenomena from phonology to discourse structure. Finally, we discuss means for making the abduction process efficient, possibilities for extending the approach to other pragmatics phenomena, and the semantics of the weights and costs in the abduction scheme.

Rule-based systems are being applied to tasks of increasing responsibility. Deductive methods are being applied to their validation, to detect flaws in these systems and to enable us to use them with more confidence. Each system of rules is encoded as a set of axioms that define the system theory. The operation of the rule language and information about the subject domain are also described in the system theory. Validation tasks, such as establishing termination, unreachability, or consistency, or verifying properties of the system, are all phrased as conjectures. If we succeed in establishing the validity of the conjecture in the system theory, we have carried out the corresponding validation task. If the proof is restricted to be sufficiently constructive, we may extract from it information other than a simple yes/no answer. For example, we may obtain a description of a situation in which an error or anomaly may occur. A method for the gradual formulation of specifications based on the attempted proof of a series of conjectures has been found to be suitable for rule-based systems. Such a specification can serve as the basis for a reengineering of the system using conventional software technology. Validation conjectures are proved or disproved by a new theorem-proving system, SNARK, which implements (nonclausal) resolution and paramodulation, an optional constructive restriction, and some facilities for proof by induction. The system has already been applied to prove properties of a number of simple rule-based systems.

A serious problem in computer database and knowledge base security is detecting and eliminating so-called inference channels. The existence of such channels enables a user with access to information classified at a low level to infer information classified at a high level, and through the transformation of low level data to high level data may provide an unacceptable information flow. In order to estimate the presence of inference channels, determine the degree of risk which they present, and find ways to eliminate them, one needs a formal model to describe them. The authors introduce abductive reasoning. Abduction provides both the basis for a formal model for the inference problem and a computational mechanism for detecting inference channels. Abduction additionally provides a framework for reasoning with approximate and uncertain information, which enables them to extend the model for inference channels by taking into account the likelihood that a person might believe some statement of interest.>

An extenston of the Knuth-Bendix algorithm for finding complete sets of reductions is described.The extension is intended to handle equational theories which can be split into two parts, R and T, such that each equation m R can be construed as a reduction and T represents an equational theory for which a finite, complete umficat~on algorithm ~s known.The extension ts demonstrated in the case when T is the theory of a fimte number of associaUve and commutatwe functions and to which the extension is presently restricted An tmplementatlon of the extended Knuth-Bendtx algorithm has produced complete sets of reductions for free commutattve groups, commutative rings wtth umt, and distributive lattices.

An important component of automated theorem-proving systems are unification algorithms which fred most general substitutions which, when apphed to two expressions, make them equivalent Functions which are associative and commutative (such as the arithmetic addition and multiphcatton functions) are often the subject of automated theorem proving An algorithm which unifies terms whose function is associative and commutauve is presented here Termmaaon, soundness, and completeness of the algorithm have been proved for a subclass of the general case.The algorithm is an efficient alternative to other methods of handling associative-commutative functions

The representation power of goal-subgoal trees and the adequacy of this form of problem reduction is considered. A number of inadequacies in the classical form are illustrated, and two versions of a syntactic procedure incorporating extensions are given. Although the form of the corrections are suggested from resolution theory results, and the value of this connection emphasized, the paper discusses the goal tree format and its extensions on an informal level.