English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

Released
Conference Paper

Basic Paramodulation and Superposition

MPS-Authors
/persons/resource/persons44474

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

/persons/resource/persons44956

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

External Resource

https://rdcu.be/dtnhe
(Publisher version)

Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

Bachmair, L., Ganzinger, H., Lynch, C., & Snyder, W. (1992). Basic Paramodulation and Superposition. In D. Kapur (Ed.), Automated Deduction - CADE-11 (pp. 462‒476). Berlin: Springer.


Cite as: https://hdl.handle.net/11858/00-001M-0000-0023-C42D-9
Abstract
We introduce a class of restrictions for the ordered paramodulation and \u000Asuperposition calculi (inspired by the ıt basic\/ strategy for narrowing), \u000Ain which paramodulation inferences are forbidden at terms introduced by \u000Asubstitutions from previous inference steps. These refinements are compatible \u000Awith standard ordering restrictions and are complete without paramodulation \u000Ainto variables or using functional reflexivity axioms. We prove refutational \u000Acompleteness in the context of deletion rules, such as simplification by \u000Arewriting (demodulation) and subsumption, and of techniques for eliminating \u000Aredundant inferences. Finally, we discuss experimental data obtained both from \u000Aa modification of Otter and from our prototype Lisp implementation.