Experiments with semantic paramodulation

William McCune*, Lawrence Henschen

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

5 Scopus citations


A semantic restriction is presented for use with paramodulation in automated theorem-proving programs. The method applies to first-order formulas with equality whole clause forms are Horn sets. In this method, an interpretation is given to the program along with the set of clauses to be refuted. The intention is to have the interpretation serve as an example to guide the search for a refutation. The semantic restriction was incorporated into an existing automated theorem-proving program, and a number of experiments were conducted on theorems in abstract algebra. Semantic paramodulation is an extension of set-of-support paramodulation. A comparison of the two strategies was used as the basis for experimentation. The semantic searches performed markedly better than the corresponding set-of-support searches in many of the comparisons. The semantic restriction seems to make the program less sensitive to the choice of rewrite rules and supported clauses.

Original languageEnglish (US)
Pages (from-to)231-261
Number of pages31
JournalJournal of Automated Reasoning
Issue number3
StatePublished - Sep 1 1985


  • Automated theorem proving
  • Horn sets
  • equality
  • paramodulation
  • semantic inference rules
  • set of support

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence


Dive into the research topics of 'Experiments with semantic paramodulation'. Together they form a unique fingerprint.

Cite this