Search results for: Torben Braüner
article
Bulletin of the Section of Logic > 2022 > 51 > 2 > 143-162
This paper is about non-labelled proof-systems for hybrid logic, that is, proofsystems where arbitrary formulas can occur, not just satisfaction statements. We give an overview of such proof-systems, focusing on analytic systems: Natural deduction systems, Gentzen sequent systems and tableau systems. We point out major results and we discuss a couple of striking facts, in particular that nonlabelled...
article
Topics in Cognitive Science > 12 > 2 > 504 - 534
We analyze four well‐known second‐order false belief tasks. Superficially, all four tasks share a common logical structure: All are based around a principle of inertia, which says that an agent's beliefs are preserved over time, unless the agent receives information to the contrary. However, a deeper analysis reveals details that are both suggestive and puzzling. First, the four tasks exemplify all...
article
Beyond Philology: An International Journal of Linguistics, Literary Studies... > 2017 > 14/1 > 69-95
In this paper we give the motivation for and discuss the design of an experiment investigating whether the acquisition of linguistic recursion helps children with Autism Spectrum Disorder (ASD) develop second-order false belief skills. We first present the relevant psychological concepts (in particular, what Theory of Mind is, and what it has to do with false beliefs) and then go on to discuss the...
chapter
Lecture Notes in Computer Science > Conceptual Structures: Standards and Practices > Applications > 184-197
In this paper, we describe a software system for learning graph-based reasoning. The system is designed for learning Peircean graphs in an interactive fashion that allows each student to proceed in his or her own pace. The student may use the built-in exercise library working from easy exercises towards harder ones, or may work at exercises of his or her own choice. The system has been successfully...
chapter
Peirce completed his work on graphical methods for reasoning within prepositional and predicate logic, but left unfinished similar systems for various modal logics. In the present paper, we put forward a system of Peircean graphs for reasoning within the modal logic S5. It is proved that our graph-based formulation of S5 is indeed equivalent to the traditional Hilbert-Frege formulation. Our choice...
chapter
This paper extends Curry-Howard interpretations of Intuitionistic Logic and Intuitionistic Linear Logic rules for recursion. The resulting term languages, the λrec-calculus and the linear λrec-calculus respectively, are given sound categorical interpretations. The embedding of proofs of Intuitionistic Logic into proofs of Intuitionistic Linear Logic given by the Girard Translation is extended with...
chapter
Lecture Notes in Computer Science > Conceptual Structures: Standards and Practices > Logic > 456-469
The first part of this paper presents a logico-algebraic reconstruction of conceptual graph fundamentals using an appropriately extended binary relation algebra. The algebraisation comprises axioms which in a straightforward and instructive fashion admit deductive reasoning by term rewriting. As an application of the described logico-algebraic framework, the second part of the paper addresses formalisation...
chapter
Usually types of PCF are interpreted as cpos and terms as continuous functions. It is then the case that non-termination of a closed term of ground type corresponds to the interpretation being bottom; we say that the semantics is adequate. We shall here present an axiomatic approach to adequacy for PCF in the sense that we will introduce categorical axioms enabling an adequate semantics to be given...
chapter
Girard worked with the category of coherence spaces and continuous stable maps and observed that the functor that forgets the linearity of linear stable maps has a left adjoint. This fundamental observation gave rise to the discovery of Linear Logic. Since then, the category of coherence spaces and linear stable maps, with the comonad induced by the adjunction, has been considered a canonical model...
chapter
In this paper we describe a solution to the problem of proving cut-elimination for FILL, a variant of exponential-free and multiplicative Linear Logic originally introduced by Hyland and de Paiva. In the work of Hyland and de Paiva, a term assignment system is used to describe the intuitionistic character of FILL and a proof of cut-elimination is barely sketched. In the present paper, as well as correcting...
chapter
In this chapter we introduce first-order hybrid logic and its proof-theory. The chapter is structured as follows. In the first section of the chapter we introduce first-order hybrid logic. In the second section we introduce a natural deduction system for first-order hybrid logic (taken from Braüner (2005b)) and in the third section we introduce an axiom system for first-order hybrid logic (also taken...
chapter
Based on tableau systems, we in this chapter prove decidability results for hybrid logic using tableau systems. The chapter is structured as follows. In the first section of the chapter we sketch the basics of tableau systems. In the second section we give a tableau-based decision procedure for a very expressive hybrid logic including the universal modality. In the third section we show how the decision...
chapter
In this chapter we compare the hybrid-logical natural deduction system given in Section 2.2 to a labelled natural deduction system for modal logic. The chapter is structured as follows. In the first section of the chapter we describe the labelled natural deduction system under consideration and in the second section we define a translation from this system to the hybrid-logical natural deduction system...
chapter
In this chapter we introduce the proof-theory of propositional hybrid logic. The chapter is structured as follows. In the first section of the chapter we sketch the basics of natural deduction systems and in the second section we introduce a natural deduction system for hybrid logic. In the third section we sketch the basics of Gentzen systems and in the fourth section we introduce a Gentzen system...
chapter
The material in this chapter is primarily of a conceptual nature, the goal of the chapter being to put into perspective hybrid logic and the proof-theory of hybrid logic. The chapter is structured as follows. In the first section we explicate what we mean when we say that a proof-system is well-behaved. In the second section we shall try to give an answer to the following question: Why does the proof-theory...
chapter
In this chapter we introduce intuitionistic hybrid logic and its proof-theory. Intuitionistic hybrid logic is hybrid modal logic over an intuitionistic logic basis instead of a classical logical basis. The chapter is structured as follows. In the first section of the chapter we introduce intuitionistic hybrid logic (this is taken from Braüner and de Paiva (2006)). In the second section we introduce...
chapter
In this chapter we compare and contrast the natural deduction system given in Section 2.2 to a modified version of a hybrid-logical natural deduction system given by Jerry Seligman. The chapter is structured as follows. In the first section of the chapter we describe the natural deduction systems under consideration, in particular, we define our version of Seligman’s system. In the second and third...
chapter
In this chapter we give the basics of hybrid logic. The chapter is structured as follows. In the first section of the chapter we give an informal motivation of hybrid logic. In the second section we give the formal syntax and semantics and we give translations forwards and backwards between hybrid logic and first-order logic. In the third section we discuss the work of Arthur Prior and describe how...
chapter
In this chapter we prove a functional completeness result for the hybrid logic of the universal modality. The chapter is structured as follows. In the first section of the chapter we describe the natural deduction system under consideration, in the second section we give an introduction to the notion of functional completeness, and in the third section we give general rule schemas for natural deduction...
