相关论文: Stalnaker's Epistemic Logic in Isabelle/HOL

Recent ideas about epistemic modals and indicative conditionals in formal semantics have significant overlap with ideas in modal logic and dynamic epistemic logic. The purpose of this paper is to show how greater interaction between formal…

In previous work [Lewitzka, Log. J. IGPL 2017], we presented a hierarchy of classical modal systems, along with algebraic semantics, for the reasoning about intuitionistic truth, belief and knowledge. Deviating from G\"odel's interpretation…

We present an automated verification of the well-known modal logic cube in Isabelle/HOL, in which we prove the inclusion relations between the cube's logics using automated reasoning tools. Prior work addresses this problem but without…

The paper investigates an evidence-based semantics for epistemic logics. It is shown that the properties of knowledge obtained from a potentially infinite body of evidence are described by modal logic S5. At the same time, the properties of…

An approach for encoding abstract dialectical frameworks and their semantics into classical higher-order logic is presented. Important properties and semantic relationships are formally encoded and proven using the proof assistant…

In recent work, Stalnaker proposes a logical framework in which belief is realized as a weakened form of knowledge. Building on Stalnaker's core insights, and using frameworks developed in previous work by Bjorndahl and Baltag et al., we…

We present a formalization of higher-order logic in the Isabelle proof assistant, building directly on the foundational framework Isabelle/Pure and developed to be as small and readable as possible. It should therefore serve as a good…

In recent work, Stalnaker proposes a logical framework in which belief is realized as a weakened form of knowledge. Building on Stalnaker's core insights, and using frameworks developed by Bjorndahl and Baltag et al., we employ topological…

Proof assistants are important tools for teaching logic. We support this claim by discussing three formalizations in Isabelle/HOL used in a recent course on automated reasoning. The first is a formalization of System W (a system of…

Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an…

This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a free logic based shallow semantic embedding of category theory by providing a formalization…

We introduce a modal logic for describing statistical knowledge, which we call statistical epistemic logic. We propose a Kripke model dealing with probability distributions and stochastic assignments, and show a stochastic semantics for the…

In this paper, we present an alternative interpretation of propositional inquisitive logic as an epistemic logic of knowing how. In our setting, an inquisitive logic formula $\alpha$ being supported by a state is formalized as "knowing how…

We present a formalization of basics related to infinite words in the generic proof assistant Isabelle/HOL. Furthermore, we present a formalization of purely morphic and morphic languages. Finally, we present a formalized definition of…

Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers. However, the expressive nature of underlying logics and esoteric structures of proof documents impede machine learning…

Standard epistemic logics introduce a modal operator K to represent knowledge, but in doing so they presuppose the logical apparatus they aim to explain. By contrast, this paper explores how logic may be derived from the structure of…

We provide algebraic semantics together with a sound and complete sequent calculus for information update due to epistemic actions. This semantics is flexible enough to accommodate incomplete as well as wrong information e.g.due to secrecy…

We derive a Prolog theorem prover for an Intuitionistic Epistemic Logic by starting from the sequent calculus {\bf G4IP} that we extend with operator definitions providing an embedding in intuitionistic propositional logic ({\bf IPC}). With…

Isabelle is an interactive theorem prover that supports a variety of logics. It represents rules as propositions (not as functions) and builds proofs by combining rules. These operations constitute a meta-logic (or `logical framework') in…

Previous research into the relation between ASP and classical logic has identified at least two different ways in which the former extends the latter. First, ASP program typically contain sets of rules that can be naturally interpreted as…