de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Ordered Chaining for Total Orderings

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44055

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

http://pubman.mpdl.mpg.de/cone/persons/resource/persons44474

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

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

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.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-AD92-2
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.