%%% ====================================================================
%%%  @LaTeX-file{
%%%     filename  = "selmanks96.ltx",
%%%     date      = "7 June 1996",
%%%     time      = "13:44:10 EDT",
%%%     author    = "David M. Jones",
%%%     email     = "jacm@theory.lcs.mit.edu",
%%%     url       = "http://theory.lcs.mit.edu/~jacm/",
%%%     address   = "Journal of the ACM
%%%                  MIT Laboratory for Computer Science
%%%                  Room NE43-316
%%%                  545 Technology Square
%%%                  Cambridge, MA 02139
%%%                  USA",
%%%     telephone = "(617) 253-5936",
%%%     FAX       = "(617) 253-3480",
%%%     checksum  = "12999 112 487 4126",
%%%     codetable = "ISO/ASCII",
%%%     supported = "yes",
%%%     docstring = "Copyright (c) 1995 by ACM, Inc.
%%%                  Permission to make digital or hard copies of part
%%%                  or all of this work for personal or classroom use
%%%                  is granted without fee provided that copies are
%%%                  not made or distributed for profit or direct
%%%                  commercial advantage and that copies bear this
%%%                  notice and the full citation on the first page.
%%%                  Copyrights for components of this work owned by
%%%                  others than ACM must be honored. Abstracting with
%%%                  credit is permitted. To copy otherwise, to
%%%                  republish, to post on servers, or to redistribute
%%%                  to lists, requires prior specific permission
%%%                  and/or a fee. Request permissions from
%%%                  Publications Dept, ACM Inc., fax +1 (212)
%%%                  869-0481, or permissions@acm.org.
%%%
%%%                  This is a LaTeX2e file.  To process it, you will
%%%                  need a copy of the acmabs document class, which is
%%%                  available via the following URL:
%%%
%%%                  http://theory.lcs.mit.edu/~jacm/acmart/acmabs.cls
%%%                  ",
%%%  }
%%% ====================================================================

\documentclass{acmabs}

\begin{document}

\Journal{Journal of the ACM}

\refkey{SelmanKS96}

\title{Knowledge Compilation and Theory Approximation}

\author{Bart Selman \and Henry Kautz}

\Pages{193--224}

\Month{March}

\Year{1996}

\Volume{43}

\Number{2}

\maketitle

\begin{abstract}

Computational 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. \par 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.

\end{abstract}

\begin{categories}

F.4.1 [\textbf{Mathematical Logic and Formal Languages}]: Mathematical
Logic; I.2.3 [\textbf{Artificial Intelligence}]: Deduction and Theorem
Proving; I.2.4 [\textbf{Artificial Intelligence}]: Knowledge
Representation Formalisms and Methods

\end{categories}

\begin{terms}

Algorithms, Experimentation, Theory

\end{terms}

\begin{keywords}

Efficient reasoning methods, Horn clauses, knowledge-based optimization,
  knowledge compilation, query evaluation, theory approximations

\end{keywords}

\end{document}
