About: CARINE

An Entity of Type: Rule105846932, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

CARINE (Computer Aided Reasoning Engine) is a first-order classical logic automated theorem prover. It was initially built for the study of the enhancement effects of the strategies delayed clause-construction (DCC) and attribute sequences (ATS) in a depth-first search based algorithm. CARINE's main search algorithm is semi-linear resolution (SLR) which is based on an iteratively-deepening depth-first search (also known as depth-first iterative-deepening (DFID)) and used in theorem provers like THEO. SLR employs DCC to achieve a high inference rate, and ATS to reduce the search space.

Property	Value
dbo:abstract	CARINE (Computer Aided Reasoning Engine) is a first-order classical logic automated theorem prover. It was initially built for the study of the enhancement effects of the strategies delayed clause-construction (DCC) and attribute sequences (ATS) in a depth-first search based algorithm. CARINE's main search algorithm is semi-linear resolution (SLR) which is based on an iteratively-deepening depth-first search (also known as depth-first iterative-deepening (DFID)) and used in theorem provers like THEO. SLR employs DCC to achieve a high inference rate, and ATS to reduce the search space. (en)
dbo:wikiPageExternalLink	http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html http://www.atpcarine.com http://portal.acm.org/citation.cfm%3Fid=1292723&coll=GUIDE&dl=GUIDE&CFID=21911086&CFTOKEN=99864762
dbo:wikiPageID	1258255 (xsd:integer)
dbo:wikiPageLength	7870 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID	1079847289 (xsd:integer)
dbo:wikiPageWikiLink	dbr:Logical_conjunction dbr:E_equational_theorem_prover dbr:First-order_logic dbr:Logical_disjunction dbr:Automated_theorem_prover dbc:Theorem_proving_software_systems dbr:Classical_logic dbr:Logical_not dbr:Logical_or
dbp:wikiPageUsesTemplate	dbt:Math dbt:Other_uses dbt:Refimprove dbt:Reflist
dct:subject	dbc:Theorem_proving_software_systems
gold:hypernym	dbr:Logic
rdf:type	yago:WikicatSearchAlgorithms yago:Abstraction100002137 yago:Act100030358 yago:Activity100407535 yago:Algorithm105847438 yago:Event100029378 yago:Procedure101023820 yago:PsychologicalFeature100023100 yago:YagoPermanentlyLocatedEntity yago:Rule105846932
rdfs:comment	CARINE (Computer Aided Reasoning Engine) is a first-order classical logic automated theorem prover. It was initially built for the study of the enhancement effects of the strategies delayed clause-construction (DCC) and attribute sequences (ATS) in a depth-first search based algorithm. CARINE's main search algorithm is semi-linear resolution (SLR) which is based on an iteratively-deepening depth-first search (also known as depth-first iterative-deepening (DFID)) and used in theorem provers like THEO. SLR employs DCC to achieve a high inference rate, and ATS to reduce the search space. (en)
rdfs:label	CARINE (en)
owl:sameAs	freebase:CARINE wikidata:CARINE https://global.dbpedia.org/id/4eLN4
prov:wasDerivedFrom	wikipedia-en:CARINE?oldid=1079847289&ns=0
foaf:isPrimaryTopicOf	wikipedia-en:CARINE
is dbo:wikiPageDisambiguates of	dbr:Carine
is dbo:wikiPageRedirects of	dbr:Delayed_Clause_Construction dbr:Semi-linear_resolution dbr:Semi-Linear_Resolution dbr:Carine_theorem_prover dbr:Delayed_clause_construction
is dbo:wikiPageWikiLink of	dbr:Resolution_(logic) dbr:Automated_theorem_proving dbr:Carine dbr:Delayed_Clause_Construction dbr:Semi-linear_resolution dbr:Semi-Linear_Resolution dbr:Carine_theorem_prover dbr:Delayed_clause_construction
is foaf:primaryTopic of	wikipedia-en:CARINE

This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License