Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-I-91-217

Deduction systems based on resolution

Eisinger, Norbert and Ohlbach, Hans J├╝rgen

MPI-I-91-217. October 1991, 68 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
A general theory of deduction systems is presented. The theory is illustrated with deduction systems based on the resolution calculus, in particular with clause graphs.

This theory distinguishes four constituents of a deduction system:
\begin{itemize}
\item
the logic, which establishes a notion of semantic entailment;
\item
the calculus, whose rules of inference provide the syntactic counterpart of entailment;
\item
the logical state transition system, which determines the representation of formulae or sets of formulae together
with their interrelationships, and also may allow additional operations reducing the search space;
\item
the control, which comprises the criteria used to choose the most promising from among all applicable inference
steps.
\end{itemize}

Much of the standard material on resolution is presented in this framework.
For the last two levels many alternatives are discussed. Appropriately adjusted notions of soundness, completeness, confluence, and Noetherianness are introduced in order to characterize the properties of particular deduction systems. For more complex deduction systems, where logical and topological phenomena interleave, such properties can be far from obvious.
Acknowledgement:
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
91-217.pdf91-217.pdfMPI-I-91-217.dvi395 KBytes; 593 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1991-217
Hide details for BibTeXBibTeX
@TECHREPORT{EisingerOhlbach91,
  AUTHOR = {Eisinger, Norbert and Ohlbach, Hans J{\"u}rgen},
  TITLE = {Deduction systems based on resolution},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-91-217},
  MONTH = {October},
  YEAR = {1991},
  ISSN = {0946-011X},
}