| Revision as of 08:09, 11 January 2005 editPaul Haroun (talk | contribs)19 editsNo edit summary← Previous edit | Revision as of 08:28, 11 January 2005 edit undoPaul Haroun (talk | contribs)19 editsNo edit summaryNext edit → | ||
| Line 1: | Line 1: | ||
| Delayed clause-construction (DCC) is a stalling strategy that enhances a theorem prover's performance by reducing the work to construct clauses to a minimum. (See ]) | Delayed clause-construction (DCC), used in the theorem prover CARINE, 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. DCC is useful when too many intermmediate clauses are being constructed and discarded in a short period of time because the operations performed to construct such short lived clauses are avoided. (See also ]) | ||
| * (has sound) | * (has sound) | ||
Revision as of 08:28, 11 January 2005
Delayed clause-construction (DCC), used in the theorem prover CARINE, 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. DCC is useful when too many intermmediate clauses are being constructed and discarded in a short period of time because the operations performed to construct such short lived clauses are avoided. (See also ATP System Carine)
- CARINE Web Site (has sound)