@prefix rdf:	<http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix dbpedia:	<http://dbpedia.org/resource/> .
@prefix opencyc:	<http://sw.opencyc.org/2008/06/10/concept/> .
dbpedia:Automated_theorem_proving	rdf:type	opencyc:Mx4rwHc9UZwpEbGdrcN5Y29ycA ,
		opencyc:Mx4rwIjnxZwpEbGdrcN5Y29ycA .
@prefix ns3:	<http://dbpedia.org/class/yago/> .
dbpedia:Automated_theorem_proving	rdf:type	ns3:FormalMethods .
@prefix owl:	<http://www.w3.org/2002/07/owl#> .
dbpedia:Automated_theorem_proving	owl:sameAs	opencyc:Mx4rvu447ZwpEbGdrcN5Y29ycA ,
		<http://rdf.freebase.com/ns/guid.9202a8c04000641f8000000000007d13> .
@prefix foaf:	<http://xmlns.com/foaf/0.1/> .
@prefix ns6:	<http://en.wikipedia.org/wiki/> .
dbpedia:Automated_theorem_proving	foaf:page	ns6:Automated_theorem_proving .
@prefix dbpprop:	<http://dbpedia.org/property/> .
dbpedia:Automated_theorem_proving	dbpprop:reference	<http://www.idsia.ch/~juergen/goedelmachine.html> ,
		<http://www.ub-net.de/cms/proverbox.html> ,
		<http://citeseer.ist.psu.edu/detlefs03simplify.html> ,
		<http://www.irit.fr/ACTIVITES/LILaC/Lotrec/> ,
		<http://www.waldmeister.org/> ,
		<http://symbolaris.com/info/KeYmaera.html> ,
		<http://dream.inf.ed.ac.uk/projects/isaplanner/> ,
		<http://metaprl.org/> ,
		<http://www.cs.man.ac.uk/~voronkov/> ,
		<http://ergo.lri.fr> ,
		<http://www.cs.ubc.ca/~babic/index_spear.htm> ,
		<http://mcs.open.ac.uk/pp2464/alligator/> ,
		<http://www.freewebs.com/riazanov/> ,
		<http://www.prover.com/products/prover_plugin/> ,
		<http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/kiv/> ,
		<http://www.ags.uni-sb.de/~leo> .
@prefix ns8:	<http://www.acumenbusiness.com/Components/ComponentsDetail.htm#> .
dbpedia:Automated_theorem_proving	dbpprop:reference	ns8:verification-validation ,
		<http://www.theorema.org/> ,
		<http://www.manchester.ac.uk/> ,
		<http://espace.library.uq.edu.au/eserv/UQ:9691/ked.pdf> .
@prefix rdfs:	<http://www.w3.org/2000/01/rdf-schema#> .
dbpedia:Automated_theorem_proving	rdfs:label	"Demostraci\u00F3n autom\u00E1tica de teoremas"@es ,
		"\u81EA\u52D5\u5B9A\u7406\u8A3C\u660E"@ja ,
		"Automatyczne dowodzenie twierdze\u0144"@pl ,
		"\u81EA\u52D5\u5B9A\u7406\u8B49\u660E"@zh ,
		"\u0410\u0432\u0442\u043E\u043C\u0430\u0442\u0438\u0447\u0435\u0441\u043A\u043E\u0435 \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432\u043E \u0442\u0435\u043E\u0440\u0435\u043C"@ru ,
		"Prova autom\u00E1tica de teoremas"@pt ,
		"D\u00E9monstration automatique de th\u00E9or\u00E8mes"@fr ,
		"Dimostrazione automatica di teoremi"@it ,
		"Automated theorem proving"@en .
@prefix dbpedia-owl:	<http://dbpedia.org/ontology/> .
dbpedia:Automated_theorem_proving	dbpedia-owl:thumbnail	<http://upload.wikimedia.org/wikipedia/commons/thumb/1/10/Agda_proof.jpg/200px-Agda_proof.jpg> ;
	dbpprop:abstract	"Prova autom\u00E1tica de teoremas (PAT) ou dedu\u00E7\u00E3o autom\u00E1tica \u00E9 a prova de teoremas matem\u00E1ticos por um programa de computador. \u00C9 atualmente a sub-\u00E1rea mais desenvolvida do racioc\u00EDnio automatizado (RA)."@pt ,
		"La demostraci\u00F3n autom\u00E1tica de teoremas que tambi\u00E9n puede ser denominada Deducci\u00F3n automatizada, es actualmente el subcampo m\u00E1s desarrollado del razonamiento autom\u00E1tico, y se encarga de la demostraci\u00F3n de teoremas matem\u00E1ticos mediante programas de ordenador."@es ,
		"\u81EA\u52D5\u5B9A\u7406\u8B49\u660E (ATP), \u76EE\u524D\u662F\u81EA\u52A8\u63A8\u7406(AR)\u4F53\u7CFB\u4E2D\u53D1\u5C55\u6700\u597D\u7684\u90E8\u5206\uFF0C\u5B83\u7684\u76EE\u7684\u662F\u4E3A\u4F7F\u7528\u7535\u5B50\u8BA1\u7B97\u673A\u7A0B\u5E8F\u6765\u8FDB\u884C\u6570\u5B66\u5B9A\u7406\u7684\u8BC1\u660E\u3002\u5BF9\u4E8E\u4E0D\u540C\u7684\u6570\u5B66\u903B\u8F91\uFF0C\u5B83\u80FD\u591F\u63A8\u8BBA\u51FA\u4E00\u4E2A\u5B9A\u7406\u662F\u6B63\u786E\u7684\uFF0C\u8FD8\u662F\u4E0D\u53EF\u8BC1\u660E\u7684\uFF0C\u6216\u8005\u9519\u8BEF\u7684\u3002"@zh ,
		"\u81EA\u52D5\u5B9A\u7406\u8A3C\u660E\uFF08Automated Theorem Proving\u3001ATP\uFF09\u3068\u306F\u3001\u81EA\u52D5\u63A8\u8AD6(AR) \u306E\u4E2D\u3067\u3082\u6700\u3082\u6210\u529F\u3057\u3066\u3044\u308B\u5206\u91CE\u3067\u3042\u308A\u3001\u30B3\u30F3\u30D4\u30E5\u30FC\u30BF\u30D7\u30ED\u30B0\u30E9\u30E0\u306B\u3088\u3063\u3066\u6570\u5B66\u7684\u5B9A\u7406\u3092\u8A3C\u660E\u3059\u308B\u3053\u3068\u3002\u30D9\u30FC\u30B9\u3068\u306A\u308B\u8AD6\u7406\u306B\u3088\u3063\u3066\u3001\u5B9A\u7406\u306E\u59A5\u5F53\u6027\u3092\u6C7A\u5B9A\u3059\u308B\u554F\u984C\u306F\u7C21\u5358\u306A\u3082\u306E\u304B\u3089\u4E0D\u53EF\u80FD\u306A\u3082\u306E\u307E\u3067\u69D8\u3005\u3067\u3042\u308B\u3002"@ja ,
		"Automated theorem proving (ATP) or automated deduction, currently the most well-developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program."@en ,
		"Automatyczne dowodzenie twierdze\u0144 (ang. automated theorem proving) to proces, w kt\u00F3rym komputer rozstrzyga czy dane twierdzenie jest dowodliwe w jakiej\u015B teorii, cz\u0119sto przy okazji generuj\u0105c jego dow\u00F3d. Twierdzenia te nale\u017C\u0105 zwykle do rachunku zda\u0144 lub rachunku predykat\u00F3w pierwszego rz\u0119du. Dla komputera wygodniejsze jest zwykle wnioskowanie w ty\u0142, cho\u0107 czasem stosuje si\u0119 te\u017C wnioskowanie w prz\u00F3d."@pl ,
		"\u0410\u0432\u0442\u043E\u043C\u0430\u0442\u0438\u0447\u0435\u0441\u043A\u043E\u0435 \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432\u043E \u0442\u0435\u043E\u0440\u0435\u043C\u00A0\u2014 \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432\u043E \u0442\u0435\u043E\u0440\u0435\u043C, \u0440\u0435\u0430\u043B\u0438\u0437\u0443\u0435\u043C\u043E\u0435 \u043F\u0440\u043E\u0433\u0440\u0430\u043C\u043C\u043D\u043E. \u0412 \u043E\u0441\u043D\u043E\u0432\u0435 \u043B\u0435\u0436\u0438\u0442 \u0430\u043F\u043F\u0430\u0440\u0430\u0442 \u043C\u0430\u0442\u0435\u043C\u0430\u0442\u0438\u0447\u0435\u0441\u043A\u043E\u0439 \u043B\u043E\u0433\u0438\u043A\u0438. \u0418\u0441\u043F\u043E\u043B\u044C\u0437\u0443\u044E\u0442\u0441\u044F \u0438\u0434\u0435\u0438 \u0442\u0435\u043E\u0440\u0438\u0438 \u0438\u0441\u043A\u0443\u0441\u0441\u0442\u0432\u0435\u043D\u043D\u043E\u0433\u043E \u0438\u043D\u0442\u0435\u043B\u043B\u0435\u043A\u0442\u0430. \u041F\u0440\u043E\u0446\u0435\u0441\u0441 \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432\u0430 \u043E\u0441\u043D\u043E\u0432\u044B\u0432\u0430\u0435\u0442\u0441\u044F \u043D\u0430 \u043B\u043E\u0433\u0438\u043A\u0435 \u0432\u044B\u0441\u043A\u0430\u0437\u044B\u0432\u0430\u043D\u0438\u0439 \u0438 \u043B\u043E\u0433\u0438\u043A\u0435 \u043F\u0440\u0435\u0434\u0438\u043A\u0430\u0442\u043E\u0432."@ru ,
		"La dimostrazione automatica di teoremi (in inglese Automated theorem proving o ATP) o deduzione automatica, \u00E8 il sottocampo pi\u00F9 sviluppato del ragionamento automatico. L'operazione consiste nella dimostrazione di teoremi matematici da parte di un programma per computer."@it ,
		"La d\u00E9monstration automatique de th\u00E9or\u00E8mes est l'activit\u00E9 d'un logiciel qui d\u00E9montre une proposition qu'on lui soumet sans l'aide de l'utilisateur."@fr ;
	rdfs:comment	"Prova autom\u00E1tica de teoremas (PAT) ou dedu\u00E7\u00E3o autom\u00E1tica \u00E9 a prova de teoremas matem\u00E1ticos por um programa de computador. \u00C9 atualmente a sub-\u00E1rea mais desenvolvida do racioc\u00EDnio automatizado (RA)."@pt ,
		"La d\u00E9monstration automatique de th\u00E9or\u00E8mes est l'activit\u00E9 d'un logiciel qui d\u00E9montre une proposition qu'on lui soumet sans l'aide de l'utilisateur."@fr ,
		"La dimostrazione automatica di teoremi (in inglese Automated theorem proving o ATP) o deduzione automatica, \u00E8 il sottocampo pi\u00F9 sviluppato del ragionamento automatico. L'operazione consiste nella dimostrazione di teoremi matematici da parte di un programma per computer."@it ,
		"Automatyczne dowodzenie twierdze\u0144 (ang. automated theorem proving) to proces, w kt\u00F3rym komputer rozstrzyga czy dane twierdzenie jest dowodliwe w jakiej\u015B teorii, cz\u0119sto przy okazji generuj\u0105c jego dow\u00F3d. Twierdzenia te nale\u017C\u0105 zwykle do rachunku zda\u0144 lub rachunku predykat\u00F3w pierwszego rz\u0119du. Dla komputera wygodniejsze jest zwykle wnioskowanie w ty\u0142, cho\u0107 czasem stosuje si\u0119 te\u017C wnioskowanie w prz\u00F3d."@pl ,
		"\u81EA\u52D5\u5B9A\u7406\u8A3C\u660E\uFF08Automated Theorem Proving\u3001ATP\uFF09\u3068\u306F\u3001\u81EA\u52D5\u63A8\u8AD6(AR) \u306E\u4E2D\u3067\u3082\u6700\u3082\u6210\u529F\u3057\u3066\u3044\u308B\u5206\u91CE\u3067\u3042\u308A\u3001\u30B3\u30F3\u30D4\u30E5\u30FC\u30BF\u30D7\u30ED\u30B0\u30E9\u30E0\u306B\u3088\u3063\u3066\u6570\u5B66\u7684\u5B9A\u7406\u3092\u8A3C\u660E\u3059\u308B\u3053\u3068\u3002\u30D9\u30FC\u30B9\u3068\u306A\u308B\u8AD6\u7406\u306B\u3088\u3063\u3066\u3001\u5B9A\u7406\u306E\u59A5\u5F53\u6027\u3092\u6C7A\u5B9A\u3059\u308B\u554F\u984C\u306F\u7C21\u5358\u306A\u3082\u306E\u304B\u3089\u4E0D\u53EF\u80FD\u306A\u3082\u306E\u307E\u3067\u69D8\u3005\u3067\u3042\u308B\u3002"@ja ,
		"\u81EA\u52D5\u5B9A\u7406\u8B49\u660E (ATP), \u76EE\u524D\u662F\u81EA\u52A8\u63A8\u7406(AR)\u4F53\u7CFB\u4E2D\u53D1\u5C55\u6700\u597D\u7684\u90E8\u5206\uFF0C\u5B83\u7684\u76EE\u7684\u662F\u4E3A\u4F7F\u7528\u7535\u5B50\u8BA1\u7B97\u673A\u7A0B\u5E8F\u6765\u8FDB\u884C\u6570\u5B66\u5B9A\u7406\u7684\u8BC1\u660E\u3002\u5BF9\u4E8E\u4E0D\u540C\u7684\u6570\u5B66\u903B\u8F91\uFF0C\u5B83\u80FD\u591F\u63A8\u8BBA\u51FA\u4E00\u4E2A\u5B9A\u7406\u662F\u6B63\u786E\u7684\uFF0C\u8FD8\u662F\u4E0D\u53EF\u8BC1\u660E\u7684\uFF0C\u6216\u8005\u9519\u8BEF\u7684\u3002"@zh ,
		"Automated theorem proving (ATP) or automated deduction, currently the most well-developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program."@en ,
		"La demostraci\u00F3n autom\u00E1tica de teoremas que tambi\u00E9n puede ser denominada Deducci\u00F3n automatizada, es actualmente el subcampo m\u00E1s desarrollado del razonamiento autom\u00E1tico, y se encarga de la demostraci\u00F3n de teoremas matem\u00E1ticos mediante programas de ordenador."@es ,
		"\u0410\u0432\u0442\u043E\u043C\u0430\u0442\u0438\u0447\u0435\u0441\u043A\u043E\u0435 \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432\u043E \u0442\u0435\u043E\u0440\u0435\u043C\u00A0\u2014 \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432\u043E \u0442\u0435\u043E\u0440\u0435\u043C, \u0440\u0435\u0430\u043B\u0438\u0437\u0443\u0435\u043C\u043E\u0435 \u043F\u0440\u043E\u0433\u0440\u0430\u043C\u043C\u043D\u043E. \u0412 \u043E\u0441\u043D\u043E\u0432\u0435 \u043B\u0435\u0436\u0438\u0442 \u0430\u043F\u043F\u0430\u0440\u0430\u0442 \u043C\u0430\u0442\u0435\u043C\u0430\u0442\u0438\u0447\u0435\u0441\u043A\u043E\u0439 \u043B\u043E\u0433\u0438\u043A\u0438. \u0418\u0441\u043F\u043E\u043B\u044C\u0437\u0443\u044E\u0442\u0441\u044F \u0438\u0434\u0435\u0438 \u0442\u0435\u043E\u0440\u0438\u0438 \u0438\u0441\u043A\u0443\u0441\u0441\u0442\u0432\u0435\u043D\u043D\u043E\u0433\u043E \u0438\u043D\u0442\u0435\u043B\u043B\u0435\u043A\u0442\u0430. \u041F\u0440\u043E\u0446\u0435\u0441\u0441 \u0434\u043E\u043A\u0430\u0437\u0430\u0442\u0435\u043B\u044C\u0441\u0442\u0432\u0430 \u043E\u0441\u043D\u043E\u0432\u044B\u0432\u0430\u0435\u0442\u0441\u044F \u043D\u0430 \u043B\u043E\u0433\u0438\u043A\u0435 \u0432\u044B\u0441\u043A\u0430\u0437\u044B\u0432\u0430\u043D\u0438\u0439 \u0438 \u043B\u043E\u0433\u0438\u043A\u0435 \u043F\u0440\u0435\u0434\u0438\u043A\u0430\u0442\u043E\u0432."@ru ;
	foaf:depiction	<http://upload.wikimedia.org/wikipedia/commons/1/10/Agda_proof.jpg> .
@prefix skos:	<http://www.w3.org/2004/02/skos/core#> .
@prefix ns12:	<http://dbpedia.org/resource/Category:> .
dbpedia:Automated_theorem_proving	skos:subject	ns12:Formal_methods ,
		ns12:Automated_theorem_proving .
@prefix ns13:	<http://www4.wiwiss.fu-berlin.de/flickrwrappr/photos/> .
dbpedia:Automated_theorem_proving	dbpprop:hasPhotoCollection	ns13:Automated_theorem_proving .
dbpedia:Automated_theorem_prover	dbpprop:redirect	dbpedia:Automated_theorem_proving .
dbpedia:Theorem_prover	dbpprop:redirect	dbpedia:Automated_theorem_proving .
dbpedia:Automated_theorem_provers	dbpprop:redirect	dbpedia:Automated_theorem_proving .
dbpedia:Automatic_proof_system	dbpprop:redirect	dbpedia:Automated_theorem_proving .
dbpedia:Automatic_theorem_prover	dbpprop:redirect	dbpedia:Automated_theorem_proving .
dbpedia:TPTP	dbpprop:redirect	dbpedia:Automated_theorem_proving .
dbpedia:Automated_deduction	dbpprop:redirect	dbpedia:Automated_theorem_proving .
dbpedia:Automated_prover	dbpprop:redirect	dbpedia:Automated_theorem_proving .
dbpedia:Automating_theorem_proving	dbpprop:redirect	dbpedia:Automated_theorem_proving .
dbpedia:Theorem-proving_systems	dbpprop:redirect	dbpedia:Automated_theorem_proving .
dbpedia:Ross_Overbeek	dbpedia-owl:knownFor	dbpedia:Automated_theorem_proving .
@prefix ns14:	<http://dbpedia.org/ontology/Person/> .
dbpedia:Ross_Overbeek	ns14:knownFor	dbpedia:Automated_theorem_proving ;
	dbpprop:knownFor	dbpedia:Automated_theorem_proving .
dbpedia:Theorem-proving	dbpprop:redirect	dbpedia:Automated_theorem_proving .
dbpedia:Theorem_proving	dbpprop:redirect	dbpedia:Automated_theorem_proving .
dbpedia:Automatic_theorem_proving	dbpprop:redirect	dbpedia:Automated_theorem_proving .
dbpedia:First-order_theorem_provers	dbpprop:redirect	dbpedia:Automated_theorem_proving .
dbpedia:Proof_assistent	dbpprop:redirect	dbpedia:Automated_theorem_proving .
dbpedia:Theorem-proving_system	dbpprop:redirect	dbpedia:Automated_theorem_proving .
@prefix yago:	<http://mpii.de/yago/resource/> .
yago:Automated_theorem_proving	owl:sameAs	dbpedia:Automated_theorem_proving .