Hyper resolution and equality axioms without function substitutions

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

When hyperresolution used with equality axioms, the function substitution axioms tend to produce myriads of new clauses whenever a positive equality literal is present. The analogue for paramodulation is the large number of potential paramodulants where the “into” term is not at the top level of its literal. In this study, we will prove that for some class of clause sets, the use of function substitution axioms can be eliminated. Analogously, paramodulation can be applied to the top level terms only.

Original languageEnglish (US)
Title of host publication10th International Conference on Automated Deduction, Proceedings
PublisherSpringer Verlag
Pages456-469
Number of pages14
Volume449 LNAI
ISBN (Print)9783540528852
DOIs
StatePublished - Jan 1 1990
Event10th International Conference on Automated Deduction, CADE 1990 - Kaiserslautern, Germany
Duration: Jul 24 1990Jul 27 1990

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume449 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other10th International Conference on Automated Deduction, CADE 1990
CountryGermany
CityKaiserslautern
Period7/24/907/27/90

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Hyper resolution and equality axioms without function substitutions'. Together they form a unique fingerprint.

Cite this