Related Experiment Video
Updated: Jul 28, 2025

Using Eye Movements Recorded in the Visual World Paradigm to Explore the Online Processing of Spoken Language
Published on: October 13, 2018
Combining Higher-Order Logic with Set Theory Formalizations
Cezary Kaliszyk1,2, Karol Pąk3
1Department of Computer Science, University of Innsbruck, Innsbruck, Austria.
Abstract:
The Isabelle Higher-order Tarski-Grothendieck object logic includes in its foundations both higher-order logic and set theory, which allows importing the libraries of Isabelle/HOL and Isabelle/Mizar. The two libraries, however, define all the basic concepts independently, which means that the results in the two are disconnected. In this paper, we align significant parts of these two libraries, by defining isomorphisms between their concepts, including the real numbers and algebraic structures. The isomorphisms allow us to transport theorems between the foundations and use the results from the libraries simultaneously.
Related Concept Videos
Deductive Reasoning
For example, a researcher can deduce specific predictions...
Inductive Reasoning
Inductive reasoning is common in descriptive science. A life scientist makes observations and records them. This data can be qualitative or...
Theorems of Pappus and Guldinus: Problem Solving
Relation between Mathematical Equations and Block Diagrams
Constraints and Statical Determinacy
Castigliano's Theorem: Problem Solving

