Delayed clause construction
- Delayed clause construction
-
Delayed Clause Construction (DCC) is a method of improving the efficiency of automated theorem provers.
Used in the CARINE theorem prover, 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 intermediate 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
Wikimedia Foundation.
2010.
Look at other dictionaries:
Changes clause — A changes clause, in government contracting, is a required clause in government construction contracts. Contents 1 Background 2 Changes clauses for construction contracts in the Federal Acquisition Regulations 3 Purposes … Wikipedia
List of mathematics articles (D) — NOTOC D D distribution D module D D Agostino s K squared test D Alembert Euler condition D Alembert operator D Alembert s formula D Alembert s paradox D Alembert s principle Dagger category Dagger compact category Dagger symmetric monoidal… … Wikipedia
CARINE — is a first order classical logic automated theorem prover. CARINE is a resolution based theorem prover initially built for the study of the enhancement effects of the strategies delayed clause construction (DCC) and attribute sequences (ATS) in a … Wikipedia
china — /chuy neuh/, n. 1. a translucent ceramic material, biscuit fired at a high temperature, its glaze fired at a low temperature. 2. any porcelain ware. 3. plates, cups, saucers, etc., collectively. 4. figurines made of porcelain or ceramic material … Universalium
China — /chuy neuh/, n. 1. People s Republic of, a country in E Asia. 1,221,591,778; 3,691,502 sq. mi. (9,560,990 sq. km). Cap.: Beijing. 2. Republic of. Also called Nationalist China. a republic consisting mainly of the island of Taiwan off the SE coast … Universalium
Nottingham Corporation Tramways — This article is about trams between 1898–1938. For trams between 1875 1897, see Nottingham and District Tramways Company Limited. For trams from 2004 onwards, see Nottingham Express Transit. Tram passing Nottingham Victoria Railway Station… … Wikipedia
Turning Stone Resort & Casino — Turning Stone Casino and Resort is a resort owned and operated by the Oneida Indian Nation in Verona, New York. The facility opened July 16, 1993 and offers golf amenities (on and off site golf courses, one of PGA quality, and an indoor golf… … Wikipedia
United States — a republic in the N Western Hemisphere comprising 48 conterminous states, the District of Columbia, and Alaska in North America, and Hawaii in the N Pacific. 267,954,767; conterminous United States, 3,022,387 sq. mi. (7,827,982 sq. km); with… … Universalium
japan — japanner, n. /jeuh pan /, n., adj., v., japanned, japanning. n. 1. any of various hard, durable, black varnishes, originally from Japan, for coating wood, metal, or other surfaces. 2. work varnished and figured in the Japanese manner. 3. Japans,… … Universalium
Japan — /jeuh pan /, n. 1. a constitutional monarchy on a chain of islands off the E coast of Asia: main islands, Hokkaido, Honshu, Kyushu, and Shikoku. 125,716,637; 141,529 sq. mi. (366,560 sq. km). Cap.: Tokyo. Japanese, Nihon, Nippon. 2. Sea of, the… … Universalium
