%%% ====================================================================
%%%  @LaTeX-file{
%%%     filename  = "murrayr93.ltx",
%%%     date      = "20 October 1995",
%%%     time      = "16:48:19 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  = "05429 113 491 4216",
%%%     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{MurrayR93}

\title{Dissolution: Making Paths Vanish}

\author{Neil~V. Murray \and Erik Rosenthal}

\Pages{504--535}

\Month{July}

\Year{1993}

\Volume{40}

\Number{3}

\maketitle

\begin{abstract}

\emph{Path dissolution}, a rule of inference that operates on formulas in
  negation normal form and that employs a representation called \emph{semantic
  graphs}, is introduced. Path dissolution has several advantages in comparison
  with many other inference technologies. In the ground case it preserves
  equivalence and is strongly complete: Any sequence of dissolution steps
  applied exhaustively to a semantic graph~$G$ will yield an equivalent
  linkless graph~$G'$. Furthermore, one need not (and cannot) restrict
  attention to conjunctive normal form (CNF) when employing dissolution: A
  single application (even to a CNF formula) generally produces a non-CNF
  formula that is more compact than any of its CNF equivalents. \par Path
  dissolution is a global rule; as such, it is employed at the first order
  level differently from the way locally-oriented techniques such as resolution
  are. Two methods for employing dissolution as an inference mechanism for
  first order logic are presented. \par Dissolution is briefly related to the
  author's theory links mechanism, the factoring of formulas with the
  distributive laws, and to analytic tableaux. Some preliminary experimental
  results are also reported.

\end{abstract}

\begin{categories}

F.4.1 [\textbf{Mathematical Logic and Formal Languages}]: Mathematical
  Logic---\emph{computational logic}; \emph{mechanical theorem
  proving}; G.2.2 [\textbf{Discrete Mathematics}]: Graph Theory; I.2.3
  [\textbf{Artificial Intelligence}]: Deduction and Theorem
  Proving---\emph{deduction}; \emph{metatheory}; \emph{resolution}

\end{categories}

\begin{terms}

Algorithms, Theory

\end{terms}

\begin{keywords}

Automated deduction, inference, matrix methods, path, Prawitz analysis

\end{keywords}

\end{document}