English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Non‐clausal Resolution and Superposition with Selection and Redundancy Criteria

MPS-Authors
/persons/resource/persons44055

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

/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. (1992). Non‐clausal Resolution and Superposition with Selection and Redundancy Criteria. In A. Voronkov (Ed.), Logic Programming and Automated Reasoning (pp. 273-284). Berlin: Springer.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0023-C430-0
Abstract
We extend previous results about resolution and superposition with ordering \u000Aconstraints and selection functions to the case of general (quantifier‐free) \u000Afirst‐order formulas with equality. The refutation completeness of our calculi \u000Ais compatible with a general and powerful redundancy criterion which includes \u000Amost (if not all) techniques for simplifying and deleting formulas. The \u000Aspectrum of first‐order theorem proving techniques covered by our results \u000Aincludes ordered resolution, positive resolution, hyper‐resolution, semantic \u000Aresolution, set‐of‐support resolution, and Knuth/Bendix completion, as well as \u000Atheir extension to general first‐order formulas. An additional feature in the \u000Alatter case is our efficient handling of equivalences as equalities on the \u000Alevel of formulas. Furthermore, our approach applies to constraint theorem \u000Aproving, including constrained resolution and theory resolution.