Misplaced Pages

Delayed clause construction: Difference between revisions

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
Browse history interactively← Previous editNext edit →Content deleted Content addedVisualWikitext
Revision as of 08:44, 11 January 2005 editPaul Haroun (talk | contribs)19 editsNo edit summary← Previous edit Revision as of 03:11, 21 February 2005 edit undoEric Herboso (talk | contribs)Extended confirmed users1,147 edits wikify, stubNext edit →
Line 1: Line 1:
'''Delayed Clause Construction''' (DCC) is a method of improving the efficiency of ]s.
⚫ 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. 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.


⚫ 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 ])


⚫ 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) * (has sound)

{{stub}}

Revision as of 03:11, 21 February 2005

Delayed Clause Construction (DCC) is a method of improving the efficiency of automated theorem provers.

Used in the theorem prover CARINE, 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: ATP System Carine, automated theorem prover

External links

This article is a stub. You can help Misplaced Pages by expanding it.