AbstractComputational efficiency is a central concern in the design of knowledge representation systems. In order to obtain efficient systems, it has been suggested that one should limit the form of the statements in the knowledge base or use an incomplete inference mechanism. The former approach is often too restrictive for practical applications, whereas the latter leads to uncertainty about exactly what can and cannot be inferred from the knowledge base. We present a third alternative, in which knowledge given in a general representation level is translated (compiled) into a tractable form -- allowing for efficient subsequent query answering.
We show how propositional logical theories can be compiled into Horn theories that approximate the original information. The approximations bound the original theory from below and above in terms of logical strength. The procedures are extended to other tractable languages (for example, binary clauses) and to the first-order case. Finally, we demonstrate the generality of our approach by compiling concept descriptions in a general frame-based language into a tractable form.
The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.
Categories and Subject Descriptors: F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving; I.2.4 [Artificial Intelligence]: Knowledge Representation Formalisms and Methods
General Terms: Algorithms, Experimentation, Theory
Additional Key Words and Phrases: Efficient reasoning methods, Horn clauses, knowledge-based optimization, knowledge compilation, query evaluation, theory approximations
Selected papers that cite this one
- Roni Khardon and Dan Roth. Learning to reason. Journal of the ACM, 44(5):697-725, September 1997.
Selected references
- Stephen A. Cook. The complexity of theorem-proving procedures. In Conference Record of Third Annual ACM Symposium on Theory of Computing, pages 151-158, Shaker Heights, Ohio, 3-5 1971 1971.
- Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, July 1960.
- William F. Dowling and Jean H. Gallier. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. Journal of Logic Programming, 1(3):267-284, October 1984.
- Nevin Heintze and Joxan Jaffar. A finite presentation theorem for approximating logic programs. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 197-209, San Francisco, California, January 1990.
- L. Henschen and L. Wos. Unit refutations and Horn sets. Journal of the ACM, 21(4):590-605, October 1974.
- Harry R. Lewis. Renaming a set of clauses as a Horn set. Journal of the ACM, 25(1):134-135, January 1978.
- Leslie G. Valiant. A theory of the learnable. Communications of the ACM, 27(11):1134-1142, November 1984.
- L. G. Valiant and V. V. Vazirani. NP is as easy as detecting unique solutions. Theoretical Computer Science, 47(1):85-93, 1986.