Matches in DBpedia 2014 for { <http://dbpedia.org/resource/Isabelle_(proof_assistant)> ?p ?o. }
Showing items 1 to 50 of
50
with 100 items per page.
- Isabelle_(proof_assistant) abstract "The Isabelle theorem prover is an interactive theorem prover, successor of the Higher Order Logic (HOL) theorem prover. It is an LCF-style theorem prover (written in Standard ML), so it is based on a small logical core guaranteeing logical correctness. Isabelle is generic: it provides a meta-logic (a weak type theory), which is used to encode object logics like First-order logic (FOL), Higher-order logic (HOL) or Zermelo–Fraenkel set theory (ZFC). Isabelle's main proof method is a higher-order version of resolution, based on higher-order unification. Though interactive, Isabelle also features efficient automatic reasoning tools, such as a term rewriting engine and a tableaux prover, as well as various decision procedures. Isabelle has been used to formalize numerous theorems from mathematics and computer science, like Gödel's completeness theorem, Gödel's theorem about the consistency of the axiom of choice, the prime number theorem, correctness of security protocols, and properties of programming language semantics. The Isabelle theorem prover is free software, released under the revised BSD license.".
- Isabelle_(proof_assistant) author Lawrence_Paulson.
- Isabelle_(proof_assistant) latestReleaseVersion "Isabelle2013-2".
- Isabelle_(proof_assistant) license BSD_licenses.
- Isabelle_(proof_assistant) programmingLanguage Standard_ML.
- Isabelle_(proof_assistant) wikiPageExternalLink afp.sourceforge.net.
- Isabelle_(proof_assistant) wikiPageExternalLink isabelle.in.tum.de.
- Isabelle_(proof_assistant) wikiPageExternalLink isarmathlib.
- Isabelle_(proof_assistant) wikiPageExternalLink isabelle.
- Isabelle_(proof_assistant) wikiPageExternalLink projects.html.
- Isabelle_(proof_assistant) wikiPageID "161886".
- Isabelle_(proof_assistant) wikiPageRevisionID "591864804".
- Isabelle_(proof_assistant) author Lawrence_Paulson.
- Isabelle_(proof_assistant) genre "Mathematics".
- Isabelle_(proof_assistant) hasPhotoCollection Isabelle_(proof_assistant).
- Isabelle_(proof_assistant) latestReleaseVersion "Isabelle2013-2".
- Isabelle_(proof_assistant) license BSD_licenses.
- Isabelle_(proof_assistant) name "Isabelle".
- Isabelle_(proof_assistant) operatingSystem "Linux, Windows, Mac OS X".
- Isabelle_(proof_assistant) programmingLanguage "Standard ML and Scala".
- Isabelle_(proof_assistant) subject Category:Free_theorem_provers.
- Isabelle_(proof_assistant) subject Category:Proof_assistants.
- Isabelle_(proof_assistant) subject Category:Theorem_proving_software_systems.
- Isabelle_(proof_assistant) type Abstraction100002137.
- Isabelle_(proof_assistant) type Code106355894.
- Isabelle_(proof_assistant) type CodingSystem106353757.
- Isabelle_(proof_assistant) type Communication100033020.
- Isabelle_(proof_assistant) type Software106566077.
- Isabelle_(proof_assistant) type Writing106359877.
- Isabelle_(proof_assistant) type WrittenCommunication106349220.
- Isabelle_(proof_assistant) type Software.
- Isabelle_(proof_assistant) type Work.
- Isabelle_(proof_assistant) type CreativeWork.
- Isabelle_(proof_assistant) type InformationEntity.
- Isabelle_(proof_assistant) comment "The Isabelle theorem prover is an interactive theorem prover, successor of the Higher Order Logic (HOL) theorem prover. It is an LCF-style theorem prover (written in Standard ML), so it is based on a small logical core guaranteeing logical correctness. Isabelle is generic: it provides a meta-logic (a weak type theory), which is used to encode object logics like First-order logic (FOL), Higher-order logic (HOL) or Zermelo–Fraenkel set theory (ZFC).".
- Isabelle_(proof_assistant) label "Isabelle (Theorembeweiser)".
- Isabelle_(proof_assistant) label "Isabelle (logiciel)".
- Isabelle_(proof_assistant) label "Isabelle (proof assistant)".
- Isabelle_(proof_assistant) label "Isabelle".
- Isabelle_(proof_assistant) sameAs Isabelle_(Theorembeweiser).
- Isabelle_(proof_assistant) sameAs Isabelle.
- Isabelle_(proof_assistant) sameAs Isabelle_(logiciel).
- Isabelle_(proof_assistant) sameAs m.015gp5.
- Isabelle_(proof_assistant) sameAs Q460340.
- Isabelle_(proof_assistant) sameAs Q460340.
- Isabelle_(proof_assistant) sameAs Isabelle_(proof_assistant).
- Isabelle_(proof_assistant) wasDerivedFrom Isabelle_(proof_assistant)?oldid=591864804.
- Isabelle_(proof_assistant) homepage isabelle.in.tum.de.
- Isabelle_(proof_assistant) isPrimaryTopicOf Isabelle_(proof_assistant).
- Isabelle_(proof_assistant) name "Isabelle".