Experiments with semantic paramodulation (Q1820597)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Experiments with semantic paramodulation |
scientific article |
Statements
Experiments with semantic paramodulation (English)
0 references
1985
0 references
A semantic restriction is presented for use with paramodulation in automated theorem-proving programs. The method applies to first-order formulas with equality whose clause forms are Horn sets. In this method, an interpretation is given to the pogram 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.
0 references
automated theorem proving
0 references
equality
0 references
Horn sets
0 references
paramodulation
0 references
semantic inference rules
0 references
set of support
0 references