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

MPI-I-93-236

Basic paramodulation

Bachmair, Leo and Ganzinger, Harald and Lynch, Christopher and Snyder, Wayne

MPI-I-93-236. September 1993, 36 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
We introduce a class of restrictions for the ordered paramodulation and superposition calculi (inspired by the {\em basic\/} strategy for narrowing), in which paramodulation inferences are forbidden at terms introduced by substitutions from previous inference steps. In addition we introduce restrictions based on term selection rules and redex orderings, which are general criteria for delimiting the terms which are available for inferences. These refinements are compatible with standard ordering restrictions and are complete without paramodulation into variables or using functional reflexivity axioms. We prove refutational completeness in the context of deletion rules, such as simplification by rewriting (demodulation) and subsumption, and of techniques for eliminating redundant inferences.
Note:
Revised version in Information and Computation 121(2), pp.~172--192, 1995
Acknowledgement:
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-93-236.pdfMPI-I-93-236.pdfMPI-I-93-236.dvi165 KBytes; 227 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/1993-236
Hide details for BibTeXBibTeX
@TECHREPORT{Bachmair-et-el-93-mpii236,
  AUTHOR = {Bachmair, Leo and Ganzinger, Harald and Lynch, Christopher and Snyder, Wayne},
  TITLE = {Basic paramodulation},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-93-236},
  MONTH = {September},
  YEAR = {1993},
  ISSN = {0946-011X},
  NOTE = {Revised version in Information and Computation 121(2), pp.~172--192, 1995},
}