%%% ====================================================================
%%%  @LaTeX-file{
%%%     filename  = "murrayr87.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  = "04101 104 463 3962",
%%%     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{MurrayR87}

\title{Inference with Path Resolution and Semantic Graphs}

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

\Pages{225--254}

\Month{April}

\Year{1987}

\Volume{34}

\Number{2}

\maketitle

\begin{abstract}

We introduce a graphical representation of quantifier-free predicate calculus
  formulas in negation normal form and a new rule of inference that employs
  this representation. The new rule, \emph{path resolution}, is an amalgamation
  of resolution and Prawitz analysis. Our goal in the design of path resolution
  is to retain some of the advantages of both Prawitz analysis and resolution
  methods, and yet to avoid to some extent their disadvantages. \par Path
  resolution allows Prawitz analysis of an arbitrary subgraph of the graph
  representing a formula. If such a subgraph is not large enough to demonstrate
  a contradiction, a path resolvent of the subgraph may be generated with
  respect to the entire graph. This generalizes the notions of large inference
  present in hyper-resolution, clash-resolution, NC-resolution, and
  UR-resolution. \par A class of subgraphs is described for which deletion of
  some of the links resolved upon preserves the spanning property.

\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{keywords}

Automated deduction, connection graph, inference, link deletion, path, Prawitz
  analysis

\end{keywords}

\end{document}
