English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  Ordered Chaining for Total Orderings

Bachmair, L., & Ganzinger, H. (1994). Ordered Chaining for Total Orderings. In A. Bundy (Ed.), Proceedings of the 12th International Conference on Automated Deduction (CADE-12) (pp. 435-450). Berlin, Germany: Springer.

Item is

Files

show Files

Locators

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

Creators

show
hide
 Creators:
Bachmair, Leo1, Author           
Ganzinger, Harald1, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 Abstract: We propose inference systems based on ordered chaining and a concept of
(global) redundancy for clauses and inferences for dealing with total
orderings. A key to the practicality of chaining techniques is the extent to
which so-called variable chainings can be restricted. We demonstrate that
ordering restrictions and the rewrite techniques which account for their
completeness considerably restrict variable chaining. For dense total orderings
we show that the techniques for eliminating unshielded variables are admissible
simplifications so that no variable chaining is needed at all. We also include
equality by combining ordered chaining with superposition.

Details

show
hide
Language(s): eng - English
 Dates: 2010-03-121994
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519607
Other: Local-ID: C1256104005ECAFC-C706EB9EE24088C2C125614C004A6FF3-BachmairGanzinger-94-cade
DOI: 10.1007/3-540-58156-1_32
BibTex Citekey: Bachmair/Ganzinger_CADE94
 Degree: -

Event

show
hide
Title: 12th International Conference on Automated Deduction
Place of Event: Nancy, France
Start-/End Date: 1994

Legal Case

show

Project information

show

Source 1

show
hide
Title: Proceedings of the 12th International Conference on Automated Deduction (CADE-12)
  Abbreviation : CADE 1994
Source Genre: Proceedings
 Creator(s):
Bundy, Alan1, Editor           
Affiliations:
1 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 435 - 450 Identifier: ISBN: 978-3-540-58156-7

Source 2

show
hide
Title: Lecture Notes in Artificial Intelligence
  Abbreviation : LNAI
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 814 Sequence Number: - Start / End Page: - Identifier: -