About: Isabelle (proof assistant)

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

Higher-order logic (HOL) automated theorem prover

Property	Value
dbo:author	dbr:Lawrence_Paulson
dbo:description	logiciel (fr) software (nl) demostrador de teoremas (es) higher-order logic (HOL) automated theorem prover (en)
dbo:developer	dbr:University_of_Cambridge dbr:Technical_University_of_Munich
dbo:genre	dbr:Mathematics
dbo:latestReleaseVersion	Isabelle2025
dbo:license	dbr:BSD_licenses
dbo:operatingSystem	dbr:Linux dbr:Microsoft_Windows dbr:MacOS
dbo:programmingLanguage	dbr:Standard_ML dbr:Scala_(programming_language)
dbo:thumbnail	wiki-commons:Special:FilePath/Isabelle_jedit.png?width=300
dbo:wikiPageExternalLink	https://isabelle.in.tum.de/ https://www.isa-afp.org/ https://isabelle.in.tum.de https://isarmathlib.org https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-189.pdf https://stackoverflow.com/tags/isabelle/ https://isabelle.in.tum.de/doc/tutorial.pdf https://link.springer.com/chapter/10.1007/BFb0000502 https://arxiv.org/abs/cs/9301105
dbo:wikiPageWikiLink	dbr:L4_microkernel_family dbr:Tobias_Nipkow dbr:Declarative_programming dbr:Standard_ML_of_New_Jersey dbr:C++ dbr:Counterexample dbr:Standard_ML dbr:Microkernel dbr:Formal_methods dbr:Resolution_(logic) dbr:Satisfiability_modulo_theories dbr:Integrated_development_environment dbr:First-order_logic dbr:University_of_Cambridge dbr:SPASS dbr:Prime_number_theorem dbr:Square_root_of_2 dbr:Type_theory dbr:Gödel's_completeness_theorem dbr:Procedural_programming dbr:Free_software dbr:Linux dbr:Mathematics dbr:Zermelo–Fraenkel_set_theory dbr:Free_Pascal dbr:OCaml dbr:Gérard_Huet dbr:Prover9 dbr:Coq dbr:Lightweight_Java dbr:C_(programming_language) dbr:Computer_science dbr:MacOS dbc:Software_using_the_BSD_license dbr:Lemma_(mathematics) dbr:Technical_University_of_Munich dbr:Model_theory dbr:ANSI_C dbr:Scala_(programming_language) dbc:Free_theorem_provers dbr:Method_of_analytic_tableaux dbr:Mizar_system dbr:Higher-order_logic dbr:Twelf dbr:Formal_verification dbr:Proof_by_contradiction dbr:Agda_(programming_language) dbc:Proof_assistants dbr:Python_(programming_language) dbr:Axiom_of_choice dbr:NICTA dbr:Metamath dbr:LEGO_(proof_assistant) dbr:E_(theorem_prover) dbr:Lean_(proof_assistant) dbr:Automated_theorem_prover dbr:Lawrence_Paulson dbr:LCF_theorem_prover dbr:Haskell_(programming_language) dbr:Formal_semantics_of_programming_languages dbr:Windows dbr:BSD_license dbr:First-order_resolution dbr:Subroutine dbr:HOL_(proof_assistant) dbr:Term_rewriting dbr:Lawrence_C._Paulson dbr:Meta-logic dbr:Tactic_(computer_science) dbr:Unification_(computing) dbr:CVC4 dbr:Security_protocol dbr:Type_soundness
dbp:author	dbr:Lawrence_Paulson
dbp:caption	Isabelle–jEdit running on macOS (en)
dbp:developer	dbr:University_of_Cambridge Technical University of Munich, et al. (en)
dbp:genre	dbr:Mathematics
dbp:latestReleaseVersion	Isabelle2025 (en)
dbp:license	dbr:BSD_licenses
dbp:name	Isabelle (en)
dbp:operatingSystem	dbr:Linux dbr:Microsoft_Windows dbr:MacOS
dbp:programmingLanguage	dbr:Standard_ML dbr:Scala_(programming_language)
dbp:screenshot	Isabelle jedit.png (en)
dbp:wikiPageUsesTemplate	dbt:Portal dbt:Start_date_and_age dbt:Reflist dbt:Notelist dbt:= dbt:Color dbt:URL dbt:Green dbt:Blue dbt:IPAc-en dbt:Further dbt:Infobox_software dbt:Official_website dbt:Refend dbt:Refbegin dbt:ML_programming dbt:Olive dbt:Issn dbt:Efn dbt:Mathbb dbt:Short_description
dct:subject	dbc:Software_using_the_BSD_license dbc:Free_theorem_provers dbc:Proof_assistants
gold:hypernym	dbr:Prover
rdf:type	owl:Thing wikidata:Q386724 wikidata:Q7397 dbo:Work schema:CreativeWork
rdfs:label	Isabelle (proof assistant) (en) Isabelle (es) Isabelle (logiciel) (fr) Isabelle (Theorembeweiser) (de) Isabelle (pt) Isabelle (ru) Isabelle (zh)
owl:sameAs	freebase:Isabelle (proof assistant) wikidata:Isabelle (proof assistant) dbpedia-de:Isabelle (proof assistant) dbpedia-fr:Isabelle (proof assistant) dbpedia-zh:Isabelle (proof assistant) dbpedia-pt:Isabelle (proof assistant) dbpedia-es:Isabelle (proof assistant) dbpedia-ru:Isabelle (proof assistant) dbpedia-global:Isabelle (proof assistant)
prov:wasDerivedFrom	wikipedia-en:Isabelle_(proof_assistant)?oldid=1290363768&ns=0
foaf:depiction	wiki-commons:Special:FilePath/Isabelle_jedit.png
foaf:homepage	http://isabelle.in.tum.de https://isabelle.in.tum.de/
foaf:isPrimaryTopicOf	wikipedia-en:Isabelle_(proof_assistant)
foaf:name	Isabelle (en)
is dbo:influenced of	dbr:Haskell
is dbo:knownFor of	dbr:Tobias_Nipkow dbr:Lawrence_Paulson
is dbo:wikiPageDisambiguates of	dbr:Isabelle_(disambiguation)
is dbo:wikiPageRedirects of	dbr:Nunchaku_(Isabelle) dbr:Sledgehammer_(Isabelle) dbr:Metis_(theorem_prover) dbr:Intelligible_semi-automated_reasoning dbr:Locale_(Isabelle) dbr:Archive_of_Formal_Proofs dbr:Isabelle_proof_assistant dbr:Isabelle_proof_assistant dbr:Isabelle/HOL dbr:Isabelle_(theorem_prover) dbr:Isabelle_AFP dbr:Isabelle_software dbr:Isabelle_theorem_prover dbr:Isar_(Isabelle) dbr:The_Archive_of_Formal_Proofs dbr:Nitpick_(Isabelle)
is dbo:wikiPageWikiLink of	dbr:Automated_reasoning dbr:Dictatorship_mechanism dbr:Finger_tree dbr:1986_in_science dbr:Standard_ML dbr:Integer dbr:Proof_assistant dbr:Type_theory dbr:Thomas_Callister_Hales dbr:Presburger_arithmetic dbr:Van_Emde_Boas_tree dbr:Coq dbr:Kepler_conjecture dbr:Nunchaku_(Isabelle) dbr:Sledgehammer_(Isabelle) dbr:Mutilated_chessboard_problem dbr:Cantor's_theorem dbr:JFreeChart dbr:Agda_(programming_language) dbr:Metamath dbr:Metis_(theorem_prover) dbr:Grigore_Roșu dbr:Lawrence_Paulson dbr:Intelligible_semi-automated_reasoning dbr:Locale_(Isabelle) dbr:Department_of_Computer_Science_and_Technology,_University_of_Cambridge dbr:Archive_of_Formal_Proofs dbr:Isabelle_(disambiguation) dbr:HOL_(proof_assistant) dbr:TLA+ dbr:Isabelle_proof_assistant dbr:Isabelle/HOL dbr:Isabelle_(theorem_prover) dbr:Isabelle_AFP dbr:Isabelle_software dbr:Isabelle_theorem_prover dbr:Isar_(Isabelle) dbr:The_Archive_of_Formal_Proofs dbr:Nitpick_(Isabelle)
is dbp:knownFor of	dbr:Tobias_Nipkow
is foaf:primaryTopic of	wikipedia-en:Isabelle_(proof_assistant)