Help Privacy Policy Disclaimer
  Advanced SearchBrowse




Journal Article

Basic Paramodulation


Bachmair,  Leo
Programming Logics, MPI for Informatics, Max Planck Society;


Ganzinger,  Harald
Programming Logics, MPI for Informatics, Max Planck Society;


Lynch,  Christopher
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

(Publisher version), 2MB

Supplementary Material (public)
There is no public supplementary material available

Bachmair, L., Ganzinger, H., Lynch, C., & Snyder, W. (1995). Basic Paramodulation. Information and Computation, 121(2), 172-192. doi:10.1006/inco.1995.1131.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-ACEC-4
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.