Isar
E822907
Isar is a structured, human-readable proof language designed for writing formal proofs within the Isabelle interactive theorem prover.
All labels observed (1)
| Label | Occurrences |
|---|---|
| Isar canonical | 4 |
How this entity was disambiguated
This entity first appeared as the object of triple T9810078 — resolving that mention is where its identity was fixed. The disambiguator weighed these candidate entities and picked the highlighted one (or “None”, minting a new entity). This is how homonymy is resolved: the same surface form can point to different entities.
NED1
Entity disambiguation (via context triple)
gpt-5-mini-2025-08-07
Target entity: Isar Context triple: [Isabelle, usesProofLanguage, Isar]
-
A.
Isar
The Isar is a major river in the Austrian and German Alps that flows through cities such as Munich before joining the Danube.
-
B.
Isar valley
The Isar valley is a scenic river valley in Bavaria, Germany, known for its picturesque landscapes, forests, and traditional towns along the Isar River.
-
C.
Hadern
Hadern is a borough in the southwest of Munich, Germany, known for its residential character and the large Waldfriedhof cemetery.
-
D.
Brackenberg
Brackenberg is an early recorded historical name for the Brocken, the highest peak in Germany’s Harz Mountains.
-
E.
Ebrach
Ebrach is a river in Bavaria, Germany, known as a tributary of the Regnitz.
- F. None of above. chosen
- G. Unsure - the case is ambiguous/there is not enough information to decide.
NED2
Entity disambiguation (via description)
gpt-5-mini-2025-08-07
Target entity: Isar Target entity description: Isar is a structured, human-readable proof language designed for writing formal proofs within the Isabelle interactive theorem prover.
-
A.
Isar
The Isar is a major river in the Austrian and German Alps that flows through cities such as Munich before joining the Danube.
-
B.
Isar valley
The Isar valley is a scenic river valley in Bavaria, Germany, known for its picturesque landscapes, forests, and traditional towns along the Isar River.
-
C.
Hadern
Hadern is a borough in the southwest of Munich, Germany, known for its residential character and the large Waldfriedhof cemetery.
-
D.
Brackenberg
Brackenberg is an early recorded historical name for the Brocken, the highest peak in Germany’s Harz Mountains.
-
E.
Ebrach
Ebrach is a river in Bavaria, Germany, known as a tributary of the Regnitz.
- F. None of above. chosen
Statements (49)
| Predicate | Object |
|---|---|
| instanceOf |
component of Isabelle
ⓘ
formal proof language ⓘ proof language ⓘ structured proof language ⓘ |
| aimsTo |
bridge gap between informal and formal proofs
ⓘ
make proofs more maintainable ⓘ make proofs more readable ⓘ |
| appliedIn |
hardware verification
ⓘ
mathematics formalization ⓘ program semantics ⓘ software verification ⓘ |
| compatibleWith | Isabelle proof automation ⓘ |
| designedFor |
Isabelle interactive theorem prover
ⓘ
linked to:
Isabelle proof assistant
|
| developedFor | interactive theorem proving ⓘ |
| documentationProvidedBy |
Isabelle/Isar reference manual
ⓘ
linked to:
Isabelle/Isar Reference Manual
|
| enables |
literate formal proofs
ⓘ
structured proof documents ⓘ |
| hasFeature |
Isabelle tactic integration
ⓘ
explicit proof structure ⓘ locale support ⓘ named assumptions ⓘ named facts ⓘ nested proofs ⓘ proof scripts ⓘ structured calculational reasoning ⓘ |
| hasProperty |
declarative
ⓘ
human-readable ⓘ structured ⓘ |
| hasSyntax |
block-structured
ⓘ
keyword-based ⓘ |
| integratedIn | Isabelle environment ⓘ |
| partOf | Isabelle proof language infrastructure ⓘ |
| relatedTo |
Isabelle/Isar reference manual
ⓘ
linked to:
Isabelle/Isar Reference Manual
|
| supports |
backward reasoning
ⓘ
case analysis ⓘ formal proofs ⓘ forward reasoning ⓘ local reasoning ⓘ machine-checked proofs ⓘ natural deduction style proofs ⓘ proof by induction ⓘ proof contexts ⓘ proof refinement ⓘ structured subproofs ⓘ |
| usedBy |
formal methods researchers
ⓘ
theorem proving practitioners ⓘ verification engineers ⓘ |
| usedIn |
Isabelle/HOL
ⓘ
Isabelle/ZF ⓘ |
How these facts were elicited
The pipeline generated the facts above by prompting gpt-5.1 with this entity's name + description and the instruction below.
Instruction
You are a knowledge base construction expert. Given a subject entity and a description of it, return factual statements that you know for the subject as a JSON list of dictionaries(triples), where keys must be "subject", "predicate" and "object". The number of facts may be very high, between 25 to 50 or more, for very popular subjects. For less popular subjects, the number of facts can be very low, like 5 or 10. # Requirements - If you don't know the subject at all, return an empty list. - If the subject is not a named entity, return an empty list. - Include at least one triple where predicate is "instanceOf". - Do not get too wordy. - Separate several objects into multiple triples with one object.
Input
Subject: Isar Description of subject: Isar is a structured, human-readable proof language designed for writing formal proofs within the Isabelle interactive theorem prover.
Referenced by (4)
Full triples — surface form annotated when it differs from this entity's canonical label.