Non‐clausal Resolution and Superposition with Selection and Redundancy Criteria

Bachmair, Leo; Ganzinger, Harald

doi:10.1007/BFb0013068

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

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;

External Resource

https://rdcu.be/dtnXY
(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. (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: https://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.