English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 Local TagsRelease HistoryDetailsSummary
  Basic Paramodulation and Superposition

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.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0023-C42D-9 Version Permalink: https://hdl.handle.net/21.11116/0000-000E-079F-8
Genre: Conference Paper

Files

show Files

Locators

show
hide
Locator:
https://rdcu.be/dtnhe (Publisher version)
Description:
-
OA-Status:
Not specified

Creators

show
hide
 Creators:
Bachmair, Leo1, Author
Ganzinger, Harald2, Author           
Lynch, Christopher3, Author           
Snyder, Wayne1, Author
Affiliations:
1External Organizations, ou_persistent22              
2Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              
3Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 1992
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: BibTex Citekey: Bachmair-et-al-92-cade
DOI: 10.1007/3-540-55602-8_185
 Degree: -

Event

show
hide
Title: 11th International Conference on Automated Deduction
Place of Event: Saratoga Springs, NY
Start-/End Date: 1992-06-15 - 1992-06-18

Legal Case

show

Project information

show

Source 1

show
hide
Title: Automated Deduction - CADE-11
  Abbreviation : CADE 1992
  Subtitle : 11th International Conference on Automated Deduction Saratoga Springs, NY, USA, June 15–18, 1992 Proceedings
Source Genre: Proceedings
 Creator(s):
Kapur, Deepak1, Editor           
Affiliations:
1 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Publ. Info: Berlin : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 462‒476 Identifier: ISBN: 978-3-540-55602-2

Source 2

show
hide
Title: Lecture Notes in Computer Science
  Abbreviation : LNCS
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 607 Sequence Number: - Start / End Page: - Identifier: -