| Revision as of 03:11, 21 February 2005 editEric Herboso (talk | contribs)Extended confirmed users1,147 edits wikify, stub← Previous edit | Latest revision as of 10:47, 29 January 2023 edit undoChristian75 (talk | contribs)Extended confirmed users, New page reviewers, Pending changes reviewers, Rollbackers114,303 edits {{R with history}} | ||
| (10 intermediate revisions by 9 users not shown) | |||
| Line 1: | Line 1: | ||
| #REDIRECT ] | |||
| '''Delayed Clause Construction''' (DCC) is a method of improving the efficiency of ]s. | |||
| {{R with history}} | |||
| Used in the ], DCC is a stalling strategy that enhances a theorem prover's performance by reducing the work to construct clauses to a minimum. Instead of constructing every conclusion (clause) of an applied inference rule, the information to construct such clause is temporarily stored until the theorem prover decides to either discard the clause or construct it. If the theorem prover decides to keep the clause, it will be constructed and stored in memory, otherwise the information to construct the clause is erased. Storing the information from which an inferred clause can be constructed require almost no additional CPU operations. However, constructing a clause '''may''' consume a lot of time. Some theorem provers spend 30%-40% of their total execution time constructing and deleting clauses. With DCC this wasted time can be salvaged. | |||
| DCC is useful when too many intermmediate clauses (especially first-order clauses) are being constructed and discarded in a short period of time because the operations performed to construct such short lived clauses are avoided. DCC may not be very effective on theorems with only propositional clauses. | |||
| ''See also'': ], ] | |||
| ==External links== | |||
| * (has sound) | |||
| {{stub}} | |||
Latest revision as of 10:47, 29 January 2023
Redirect to:
- With history: This is a redirect from a page containing substantive page history. This page is kept as a redirect to preserve its former content and attributions. Please do not remove the tag that generates this text (unless the need to recreate content on this page has been demonstrated), nor delete this page.
- This template should not be used for redirects having some edit history but no meaningful content in their previous versions, nor for redirects created as a result of a page merge (use {{R from merge}} instead), nor for redirects from a title that forms a historic part of Misplaced Pages (use {{R with old history}} instead).