Experiments with the hot list strategy

PDF Version Also Available for Download.

Description

Experimentation strongly suggests that, for attacking deep questions and hard problems with the assistance of an automated reasoning program, the more effective paradigms rely on the retention of deduced information. A significant obstacle ordinarily presented by such a paradigm is the deduction and retention of one or more needed conclusions whose complexity sharply delays their consideration. To mitigate the severity of the cited obstacle, the author formulates and features in this report the hot list strategy. The hot list strategy asks the researcher to choose, usually from among the input statements, one or more clauses that are conjectured to play ... continued below

Physical Description

75 p.

Creation Information

Wos, L. October 1, 1997.

Context

This report is part of the collection entitled: Office of Scientific & Technical Information Technical Reports and was provided by UNT Libraries Government Documents Department to Digital Library, a digital repository hosted by the UNT Libraries. More information about this report can be viewed below.

Who

People and organizations associated with either the creation of this report or its content.

Author

Sponsor

Publisher

Provided By

UNT Libraries Government Documents Department

Serving as both a federal and a state depository library, the UNT Libraries Government Documents Department maintains millions of items in a variety of formats. The department is a member of the FDLP Content Partnerships Program and an Affiliated Archive of the National Archives.

Contact Us

What

Descriptive information to help identify this report. Follow the links below to find similar items on the Digital Library.

Description

Experimentation strongly suggests that, for attacking deep questions and hard problems with the assistance of an automated reasoning program, the more effective paradigms rely on the retention of deduced information. A significant obstacle ordinarily presented by such a paradigm is the deduction and retention of one or more needed conclusions whose complexity sharply delays their consideration. To mitigate the severity of the cited obstacle, the author formulates and features in this report the hot list strategy. The hot list strategy asks the researcher to choose, usually from among the input statements, one or more clauses that are conjectured to play a key role for assignment completion. The chosen clauses - conjectured to merit revisiting, again and again - are placed in an input list of clauses, called the hot list. When an automated reasoning program has decided to retain a new conclusion C - before any other clause is chosen to initiate conclusion drawing - the presence of a nonempty hot list (with an appropriate assignment of the input parameter known as heat) causes each inference rule in use to be applied to C together with the appropriate number of members of the hot list. Members of the hot list are used to complete applications of inference rules and not to initiate applications. The use of the hot list strategy thus enables an automated reasoning program to briefly consider a newly retained conclusion whose complexity would otherwise prevent its use for perhaps many CPU-hours. To give evidence of the value of the strategy, the author focuses on four contexts: (1) dramatically reducing the CPU time required to reach a desired goal; (2) finding a proof of a theorem that had previously resisted all but the more inventive automated attempts; (3) discovering a proof that is more elegant than previously known; and (4) answering a question that had steadfastly eluded researchers relying on an automated reasoning program.

Physical Description

75 p.

Notes

OSTI as DE98002717

Source

  • Other Information: PBD: Oct 1997

Language

Item Type

Identifier

Unique identifying numbers for this report in the Digital Library or other systems.

  • Other: DE98002717
  • Report No.: ANL/MCS-TM--232
  • Grant Number: W-31-109-ENG-38
  • DOI: 10.2172/565657 | External Link
  • Office of Scientific & Technical Information Report Number: 565657
  • Archival Resource Key: ark:/67531/metadc696839

Collections

This report is part of the following collection of related materials.

Office of Scientific & Technical Information Technical Reports

What responsibilities do I have when using this report?

When

Dates and time periods associated with this report.

Creation Date

  • October 1, 1997

Added to The UNT Digital Library

  • Aug. 14, 2015, 8:43 a.m.

Description Last Updated

  • Dec. 15, 2015, 12:05 p.m.

Usage Statistics

When was this report last used?

Yesterday: 0
Past 30 days: 0
Total Uses: 3

Interact With This Report

Here are some suggestions for what to do next.

Start Reading

PDF Version Also Available for Download.

Citations, Rights, Re-Use

Wos, L. Experiments with the hot list strategy, report, October 1, 1997; Illinois. (digital.library.unt.edu/ark:/67531/metadc696839/: accessed August 17, 2017), University of North Texas Libraries, Digital Library, digital.library.unt.edu; crediting UNT Libraries Government Documents Department.