activity
20182025
most citedA Henkin-style completeness proof for the modal logic S5

17 citations · 24 across the 8 of their papers we have counts for

collaborators

8 papers

physics.hist-ph2025

Naturalistic intuitionism for physics

Bruno Bentzen, Flavio Del Santo, Nicolas Gisin

Recently, a novel intuitionistic reconstruction of the foundations of physics has been primarily developed by Nicolas Gisin and Flavio Del Santo drawing on naturalism. Our goal in…

cs.LO2023★ 1 cited

Verified completeness in Henkin-style for intuitionistic propositional logic

Huayu Guo, Dongheng Chen, Bruno Bentzen

This paper presents a formalization of the classical proof of completeness in Henkin-style developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke mode…

cs.CL2022★ 1 cited

BTPK-based interpretable method for NER tasks based on Talmudic Public Announcement Logic

Yulin Chen, Beishui Liao, Bruno Bentzen +4

As one of the basic tasks in natural language processing (NLP), named entity recognition (NER) is an important basic tool for downstream tasks of NLP, such as information extractio…

math.HO2020★ 2 cited

Frege's theory of types

Bruno Bentzen

It is often claimed that the theory of function levels proposed by Frege in Grundgesetze der Arithmetik anticipates the hierarchy of types that underlies Church's simple theory of…

math.HO2020★ 3 cited

Sense, reference, and computation

Bruno Bentzen

In this paper, I revisit Frege's theory of sense and reference in the constructive setting of the meaning explanations of type theory, extending and sharpening a program--value ana…

cs.LO2019

Naive cubical type theory

Bruno Bentzen

This paper proposes a way of doing type theory informally, assuming a cubical style of reasoning. It can thus be viewed as a first step toward a cubical alternative to the program…

cs.LO2019★ 17 cited

A Henkin-style completeness proof for the modal logic S5

Bruno Bentzen

This paper presents a recent formalization of a Henkin-style completeness proof for the propositional modal logic S5 using the Lean theorem prover. The proof formalized is close to…

cs.LO2018

Cubical informal type theory: the higher groupoid structure

Bruno Bentzen

Following a project of developing conventions and notations for informal type theory carried out in the homotopy type theory book for a framework built out of an augmentation of co…