About: Automated proof checking

An Entity of Type: Thing, from Named Graph: http://dbpedia.org, within Data Space: dbpedia-live.demo.openlinksw.com

Software tool to assist with the development of formal proofs by human-machine collaboration

Property	Value
dbo:description	software tool to assist with the development of formal proofs by human-machine collaboration (en) categoria di software per la logica matematica (it) demostración interactiva de teoremas (es) 通过人机协作协助开发形式化证明的软件工具 (zh) ilo por helpi pruvi teoremojn (eo) Computerprogramm zur Erzeugung und Überprüfung von mathematischen Beweisen (de) tarkvara, mis aitab luua formaalseid tõestusi läbi inimese ja arvuti koostöö (et) logiciel permettant l'écriture et la vérification de preuves mathématiques (fr)
dbo:thumbnail	wiki-commons:Special:FilePath/CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png?width=300
dbo:wikiPageExternalLink	http://www.dcs.ed.ac.uk/home/lego/ http://hol.sourceforge.net/ https://theoremprover-museum.github.io/ https://www.ias.ac.in/article/fulltext/sadh/034/01/0003-0025 http://gtps.math.cmu.edu/tps.html http://www.mcs.anl.gov/research/projects/AR/others.html https://www.cs.ru.nl/~freek/comparison/comparison.pdf https://www.cs.ru.nl/~freek/digimath/bycategory.html%23tacticprover https://www.cs.ru.nl/~janz/yarrow/ http://www.dmoz.org/Science/Math/Logic_and_Foundations/Computational_Logic/Logical_Frameworks/ http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/interactiveTheoremProvingForAgdaUsers.html http://adam.chlipala.net/cpdt/html/Intro.html http://www.informatik.uni-ulm.de/ki/typelab.html http://www.nuprl.org/Intro/others.html https://web.archive.org/web/20070727062855/http:/www.ncc.up.pt/~nam/aulas/0506/t_coq/barendregt01proofassistants.pdf https://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng/atp/systems/0.html http://www-formal.stanford.edu/clt/ARS/Pages/systems.html http://www.ncc.up.pt/~nam/aulas/0506/t_coq/barendregt01proofassistants.pdf https://www.cs.cmu.edu/~fp/papers/handbook01.pdf http://video.ias.edu/univalent/appel https://www.cs.cmu.edu/~fp/lfs-impl.html https://github.com/johnyf/tool_lists/blob/master/verification_synthesis.md%23theorem-provers
dbo:wikiPageInterLanguageLink	dbpedia-de:Maschinengestütztes_Beweisen
dbo:wikiPageWikiLink	dbr:Microsoft_Research dbr:Tobias_Nipkow dbr:Isabelle_(proof_assistant) dbr:Natural_deduction dbr:C++ dbr:Cornell_University dbr:Moscow_ML dbr:Standard_ML dbr:F*_(programming_language) dbr:Satisfiability_modulo_theories dbr:University_of_Cambridge dbr:Automated_theorem_proving dbr:Code_generation_(compiler) dbc:Argument_technology dbr:Computer-assisted_proof dbr:Tarski–Grothendieck_set_theory dbr:Prototype_Verification_System dbr:Matita dbr:Matt_Kaufmann dbr:Computer dbr:Emacs dbr:Free_Pascal dbr:OCaml dbr:Chalmers_University_of_Technology dbr:Coq dbr:Dependent_type dbr:Formal_proof dbr:HOL_Light dbr:MINLOG dbr:Jape_(software) dbr:Computer_science dbr:DMOZ dbc:Automated_theorem_proving dbr:User_interface dbr:Visual_Studio_Code dbr:University_of_Edinburgh dbr:Mathematical_logic dbr:Common_Lisp dbr:QED_manifesto dbr:Scala_(programming_language) dbr:PhoX dbr:SRI_International dbr:Mizar_system dbr:Higher-order_logic dbr:Twelf dbr:Formal_verification dbr:Lego dbr:J_Strother_Moore dbr:Agda_(programming_language) dbc:Proof_assistants dbr:JEdit dbr:Metamath dbr:LEGO_(proof_assistant) dbr:ACL2 dbr:Lean_(proof_assistant) dbr:Poly/ML dbr:Frank_Pfenning dbr:INRIA dbr:LCF_theorem_prover dbr:Haskell_(programming_language) dbr:Białystok_University dbr:Leonardo_de_Moura dbr:Technische_Universität_München dbr:Albatross_(programming_language) dbr:Idris_(programming_language) dbr:HOL_theorem_prover dbr:BSD-style_license dbr:Gtk dbr:HOL4 dbr:NuPRL dbr:ProofPower dbr:Randy_Pollack dbr:Isabelle_theorem_prover dbr:Larry_Paulson dbr:Gothenburg_University dbr:Q0_Logic dbr:Proof_automation dbr:Carsten_Schürmann dbr:De_Bruijn_criterion dbr:File:CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png dbr:Makarius_Wenzel dbr:Proof_by_reflection
dbp:wikiPageUsesTemplate	dbt:Cite_book dbt:Cite_web dbt:Reflist dbt:Anchor dbt:Partial dbt:See_also dbt:For dbt:Missing_information dbt:No dbt:Unknown dbt:N/a dbt:Yes dbt:Not_yet dbt:Distinguish dbt:R_from_long_name dbt:R_from_merge dbt:Cn dbt:GBurl dbt:Harvid dbt:Harvnb dbt:More_footnotes dbt:Rcat_shell dbt:External_links dbt:Annotated_link dbt:Short_description
dct:subject	dbc:Argument_technology dbc:Automated_theorem_proving dbc:Proof_assistants
gold:hypernym	dbr:Tool
rdfs:label	Automated proof checking (en) Proof assistant (en) Demostración interactiva de teoremas (es) Assistant de preuve (fr) System wspomagający dowodzenie twierdzeń (pl) Инструмент интерактивного доказательства теорем (ru)
rdfs:seeAlso	dbr:Computer-assisted_proof dbr:Dependent_type
owl:differentFrom	dbr:Interactive_proof_system
owl:sameAs	freebase:Automated proof checking yago-res:Automated proof checking wikidata:Automated proof checking dbpedia-fr:Automated proof checking dbpedia-es:Automated proof checking dbpedia-ru:Automated proof checking dbpedia-pl:Automated proof checking dbpedia-global:Automated proof checking dbr:Automated proof checking
prov:wasDerivedFrom	wikipedia-en:Automated_proof_checking?oldid=977146153&ns=0 wikipedia-en:Proof_assistant?oldid=1291974133&ns=0
foaf:depiction	wiki-commons:Special:FilePath/CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png
foaf:isPrimaryTopicOf	wikipedia-en:Automated_proof_checking wikipedia-en:Proof_assistant
is dbo:genre of	dbr:Jape_(software) dbr:Coq_(software)
is dbo:wikiPageRedirects of	dbr:Automated_proof_checker dbr:Automated_proof_verifier dbr:Automated_proof_verifiicator dbr:Automated_theorem_check dbr:Automated_theorem_checker dbr:Automated_theorem_checkers dbr:Automated_theorem_checking dbr:Automated_theorem_verification dbr:Automated_theorem_verificator dbr:Automated_theorem_verifier dbr:Automated_theorem_verifying dbr:Automated_proof_checking dbr:Automated_proof_checking dbr:Theorem_checker dbr:Theorem_checking dbr:List_of_interactive_theorem_provers dbr:List_of_proof_assistants dbr:Machine-verified_proof dbr:Interactive_proof_assistant dbr:Interactive_theorem_prover dbr:Interactive_theorem_proving dbr:Interactive_theorem_proving_software dbr:Proof_assistants dbr:Proof_assistent dbr:Proof_assitants dbr:Proof_checker dbr:Proof_checking dbr:Proof_editor dbr:Proof_script dbr:Proof_verification dbr:Proof_verifier
is dbo:wikiPageWikiLink of	dbr:Backward_chaining dbr:French_Institute_for_Research_in_Computer_Science_and_Automation dbr:Automated_reasoning dbr:Normalisation_by_evaluation dbr:Classification_of_finite_simple_groups dbr:Computational_mathematics dbr:Disjoint-set_data_structure dbr:Gödel's_ontological_proof dbr:Standard_ML dbr:F*_(programming_language) dbr:Pick's_theorem dbr:Intuitionistic_type_theory dbr:Integer dbr:Mathematical_proof dbr:First-order_logic dbr:Applications_of_artificial_intelligence dbr:Automated_theorem_proving dbr:Gödel's_incompleteness_theorems dbr:Type_theory dbr:Logical_machine dbr:Alloy_(specification_language) dbr:Computer-assisted_proof dbr:OpenCog dbr:SIGPLAN dbr:Matita dbr:Mathematics dbr:Thomas_Callister_Hales dbr:Interactive_Theorem_Proving_(conference) dbr:ATS_(programming_language) dbr:List_of_tools_for_static_code_analysis dbr:Georges_Gonthier dbr:Heyting_arithmetic dbr:Proof_compression dbr:Coq dbr:Dependent_type dbr:Formal_proof dbr:Automath dbr:HOL_Light dbr:MINLOG dbr:De_Bruijn_index dbr:Jape_(software) dbr:Theorem_prover dbr:List_of_pioneers_in_computer_science dbr:Automated_proof_checker dbr:Automated_proof_verifier dbr:Automated_proof_verifiicator dbr:Automated_theorem_check dbr:Automated_theorem_checker dbr:Automated_theorem_checkers dbr:Automated_theorem_checking dbr:Automated_theorem_verification dbr:Automated_theorem_verificator dbr:Automated_theorem_verifier dbr:Automated_theorem_verifying dbr:Feit–Thompson_theorem dbr:Mutilated_chessboard_problem dbr:IsaPlanner dbr:History_of_type_theory dbr:QED_manifesto dbr:PhoX dbr:Mizar_system dbr:Realizability dbr:Euclid–Euler_theorem dbr:Formal_verification dbr:Four_color_theorem dbr:Philosophy_of_mathematics dbr:Calculus_of_constructions dbr:Jeremy_Avigad dbr:Glossary_of_artificial_intelligence dbr:Homotopy_type_theory dbr:Metamath dbr:Michael_Fourman dbr:LEGO_(proof_assistant) dbr:ALF_(proof_assistant) dbr:Blakers–Massey_theorem dbr:Nuprl dbr:Timeline_of_artificial_intelligence dbr:Lean_(proof_assistant) dbr:Dafny dbr:Luigia_Carlucci_Aiello dbr:Automated_proof_checking dbr:Idris_(programming_language) dbr:HOL_(proof_assistant) dbr:WireGuard dbr:Condensed_mathematics dbr:Choreographic_programming dbr:Theorem_checker dbr:Theorem_checking dbr:List_of_interactive_theorem_provers dbr:List_of_proof_assistants dbr:Machine-verified_proof dbr:Interactive_proof_assistant dbr:Interactive_theorem_prover dbr:Interactive_theorem_proving dbr:Interactive_theorem_proving_software dbr:Proof_assistants dbr:Proof_assistent dbr:Proof_assitants dbr:Proof_checker dbr:Proof_checking dbr:Proof_editor dbr:Proof_script dbr:Proof_verification dbr:Proof_verifier
is dbp:family of	dbr:Lean_(proof_assistant)
is dbp:genre of	dbr:Jape_(software) dbr:Coq_(software)
is rdfs:seeAlso of	dbr:Automated_theorem_proving dbr:Argument_technology dbr:Computer-assisted_proof dbr:Dependent_type dbr:Coq_(software) dbr:Lean_(proof_assistant)
is owl:differentFrom of	dbr:Interactive_proof_system
is foaf:primaryTopic of	wikipedia-en:Automated_proof_checking wikipedia-en:Proof_assistant