4 papers
Makkai's lost proof of projectivity of N in the free topos
Henrik Forssell, Peter LeFanu Lumsdaine, Andrew W. Swan
We give a categorical proof of the projectivity of in the free topos -- in proof-theoretic terms, the rule of countable choice for intuitionistic higher-order logic -- based on…
On Equivalence and Cores for Incomplete Databases in Open and Closed Worlds
Henrik Forssell, Evgeny Kharlamov, Evgenij Thorstensen
Data exchange heavily relies on the notion of incomplete database instances. Several semantics for such instances have been proposed and include open (OWA), closed (CWA), and open-…
Generating Ontologies from Templates: A Rule-Based Approach for Capturing Regularity
Henrik Forssell, Christian Kindermann, Daniel P. Lupp +2
We present a second-order language that can be used to succinctly specify ontologies in a consistent and transparent manner. This language is based on ontology templates (OTTR), a…
Constructive completeness and non-discrete languages
Henrik Forssell, Christian Espíndola
We give an analysis and generalizations of some long-established constructive completeness results in terms of categorical logic and pre-sheaf and sheaf semantics. The purpose is i…