Deutsch
 
Benutzerhandbuch Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

Non‐clausal Resolution and Superposition with Selection and Redundancy Criteria

MPG-Autoren
/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;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-0023-C430-0
Zusammenfassung
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.