About: Automated proof checking

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

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://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 http://www.ncc.up.pt/~nam/aulas/0506/t_coq/barendregt01proofassistants.pdf https://www.cs.cmu.edu/~fp/papers/handbook01.pdf http://hol.sourceforge.net/ https://theoremprover-museum.github.io/ http://gtps.math.cmu.edu/tps.html http://www-formal.stanford.edu/clt/ARS/Pages/systems.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 https://www.ias.ac.in/article/fulltext/sadh/034/01/0003-0025 http://www.mcs.anl.gov/research/projects/AR/others.html
dbo:wikiPageInterLanguageLink	dbpedia-de:Maschinengestütztes_Beweisen
dbo:wikiPageWikiLink	dbr:Higher-order_logic dbr:Metamath dbr:Tarski–Grothendieck_set_theory dbr:Computer dbr:Prototype_Verification_System dbr:Computer-assisted_proof dbr:C++ dbr:Computer_science dbr:Cornell_University dbr:Mathematical_logic dbr:Microsoft_Research dbr:SRI_International dbr:Scala_(programming_language) dbr:University_of_Cambridge dbr:University_of_Edinburgh dbr:HOL_Light dbr:Mizar_system dbr:Leonardo_de_Moura dbr:MINLOG dbc:Proof_assistants dbr:Formal_verification dbr:Agda_(programming_language) dbr:Automated_theorem_proving dbr:Chalmers_University_of_Technology dbr:Idris_(programming_language) dbr:Isabelle_(proof_assistant) dbr:Standard_ML dbr:Common_Lisp dbr:Lego dbr:Formal_proof dbr:Tobias_Nipkow dbr:Jape_(software) dbr:DMOZ dbr:User_interface dbr:Natural_deduction dbr:Lean_(proof_assistant) dbr:Code_generation_(compiler) dbr:Emacs dbr:Frank_Pfenning dbr:Visual_Studio_Code dbr:Free_Pascal dbr:Matita dbr:F*_(programming_language) dbr:OCaml dbr:PhoX dbc:Automated_theorem_proving dbr:JEdit dbr:J_Strother_Moore dbr:Matt_Kaufmann dbr:Coq dbr:ACL2 dbr:Dependent_type dbr:Satisfiability_modulo_theories dbr:LEGO_(proof_assistant) dbr:QED_manifesto dbr:Twelf dbr:HOL_theorem_prover dbr:Moscow_ML dbr:Albatross_(programming_language) dbc:Argument_technology dbr:INRIA dbr:LCF_theorem_prover dbr:Technische_Universität_München dbr:Poly/ML dbr:BSD-style_license dbr:Haskell_(programming_language) dbr:Proof_automation dbr:Q0_Logic dbr:Białystok_University dbr:Gtk dbr:Larry_Paulson dbr:HOL4 dbr:Gothenburg_University dbr:Isabelle_theorem_prover dbr:NuPRL dbr:Randy_Pollack dbr:ProofPower 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:Not_yet dbt:Anchor dbt:Annotated_link dbt:Cite_web dbt:Cn dbt:Distinguish dbt:External_links dbt:For dbt:GBurl dbt:Harvid dbt:Harvnb dbt:Hatnote_group dbt:Missing_information dbt:More_footnotes dbt:N/a dbt:No dbt:Partial dbt:R_from_long_name dbt:R_from_merge dbt:Rcat_shell dbt:Redirect dbt:Reflist dbt:See_also dbt:Short_description dbt:Unknown dbt:Yes
dct:subject	dbc:Proof_assistants dbc:Automated_theorem_proving dbc:Argument_technology
gold:hypernym	dbr:Tool
rdf:type	owl:Thing owl:Thing
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-es:Automated proof checking dbpedia-pl:Automated proof checking dbpedia-fr:Automated proof checking dbpedia-ru:Automated proof checking dbpedia-global:Automated proof checking
prov:wasDerivedFrom	wikipedia-en:Proof_assistant?oldid=1311879597&ns=0 wikipedia-en:Automated_proof_checking?oldid=977146153&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:Coq_(software) dbr:Jape_(software)
is dbo:wikiPageRedirects of	dbr:Automated_proof_checking dbr:Automated_proof_checking 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 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:Machine-verified_proof dbr:Interactive_proof_assistant dbr:Interactive_theorem_prover dbr:Interactive_theorem_proving dbr:Interactive_theorem_proving_software dbr:List_of_interactive_theorem_provers dbr:List_of_proof_assistants dbr:Theorem_checker dbr:Theorem_checking
is dbo:wikiPageWikiLink of	dbr:Pick's_theorem dbr:Heyting_arithmetic dbr:Feit–Thompson_theorem dbr:Nuprl dbr:HOL_(proof_assistant) dbr:Metamath dbr:Mathematics dbr:Jeremy_Avigad dbr:SIGPLAN dbr:Computer-assisted_proof dbr:Philosophy_of_mathematics dbr:HOL_Light dbr:Logical_machine dbr:Mizar_system dbr:Blakers–Massey_theorem dbr:MINLOG dbr:Formal_verification dbr:Integer dbr:Mathematical_proof dbr:Automated_reasoning dbr:Automated_theorem_proving dbr:Idris_(programming_language) dbr:Standard_ML dbr:Type_theory dbr:Michael_Fourman dbr:Formal_proof dbr:Georges_Gonthier dbr:Interactive_Theorem_Proving_(conference) dbr:Applications_of_artificial_intelligence dbr:Jape_(software) dbr:Gödel's_incompleteness_theorems dbr:Gödel's_ontological_proof dbr:Alloy_(specification_language) dbr:Homotopy_type_theory dbr:Dafny dbr:Lean_(proof_assistant) dbr:Calculus_of_constructions dbr:WireGuard dbr:Condensed_mathematics dbr:French_Institute_for_Research_in_Computer_Science_and_Automation dbr:List_of_pioneers_in_computer_science dbr:Intuitionistic_type_theory dbr:Backward_chaining dbr:Computational_mathematics dbr:Disjoint-set_data_structure dbr:Mutilated_chessboard_problem dbr:Matita dbr:Classification_of_finite_simple_groups dbr:OpenCog dbr:First-order_logic dbr:Four_color_theorem dbr:F*_(programming_language) dbr:PhoX dbr:ALF_(proof_assistant) dbr:History_of_type_theory dbr:ATS_(programming_language) dbr:Thomas_Callister_Hales dbr:Coq dbr:Realizability dbr:Automath dbr:De_Bruijn_index dbr:List_of_tools_for_static_code_analysis dbr:Dependent_type dbr:Timeline_of_artificial_intelligence dbr:LEGO_(proof_assistant) dbr:QED_manifesto dbr:Theorem_prover dbr:IsaPlanner dbr:Normalisation_by_evaluation dbr:Euclid–Euler_theorem dbr:Luigia_Carlucci_Aiello dbr:Automated_proof_checking dbr:Choreographic_programming dbr:Proof_compression dbr:Glossary_of_artificial_intelligence 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 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:Machine-verified_proof dbr:Interactive_proof_assistant dbr:Interactive_theorem_prover dbr:Interactive_theorem_proving dbr:Interactive_theorem_proving_software dbr:List_of_interactive_theorem_provers dbr:List_of_proof_assistants dbr:Theorem_checker dbr:Theorem_checking
is dbp:family of	dbr:Lean_(proof_assistant)
is dbp:genre of	dbr:Coq_(software) dbr:Jape_(software)
is rdfs:seeAlso of	dbr:Argument_technology dbr:Computer-assisted_proof dbr:Automated_theorem_proving dbr:Coq_(software) dbr:Lean_(proof_assistant) dbr:Dependent_type
is owl:differentFrom of	dbr:Interactive_proof_system
is foaf:primaryTopic of	wikipedia-en:Automated_proof_checking wikipedia-en:Proof_assistant