Accession Number:

AD0730714

Title:

Primary Paramodulation.

Descriptive Note:

Technical rept.,

Corporate Author:

NAVAL WEAPONS LAB DAHLGREN VA

Report Date:

1971-05-01

Pagination or Media Count:

22.0

Abstract:

Computers can directly use mathematical logic, that is first-order predicate calculus, in decision making and problem solving by the application of proof strategies involving resolution and paramodulation. A new category of problem solving strategies is defined which has the interesting and unusual property that refutations are formed by mixing certain primary paramodulants with resolvents obtained from any complete strategy in the predicate calculus without equality. Also, a new and easily applied technique is given for verifying that subsumed clauses can be eliminated from deductions. This technique is applied to all the strategies considered in this paper. Author

Subject Categories:

  • Computer Programming and Software
  • Bionics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE