Theory of mind (ToM) is the ability to attribute and reason about unobservable mental states of others, such as knowledge, beliefs, and intentions. ToM is needed in social interactions, negotiations, cooperation, and deception, but there is a limit to the recursive depth of ToM attributions humans can make. Researchers in epistemic logic classically assume that agents have common knowledge of honesty and perfect rationality, whereas humans lie and have ToM limitations. In our present work, we bridge this gap by developing a sound and strongly complete dynamic epistemic logic that models both lying and human ToM limitations. The design of our logic is inspired by findings from prior behavioural research. Our logic makes use of action models to model belief change caused by lying and other types of announcements. Using theoretical examples, we show how a listener deals with lies that she cannot understand due to her ToM limits.
In this paper, we investigate dynamic modal logics with global and local dynamic operations, which update the accessibility relation of a graph model. We introduce the hybrid logic of global link variations, which involves dynamic operators of global link cutting, adding and rotating simultaneously. We provide the Hilbert-style calculus 𝖢_𝖦𝖫𝖵 and prove that it is sound and strongly complete with respect to by constructing a family of canonical models inductively. We study the hybrid extensions of the logic of definable link deletion introduced by Li (2020). We provide a sound and complete tableau calculus 𝒯((@)) for the logic (@) . Then we extend (@) to the logics (@,X) of local link variations and provide them with sound and complete tableau calculi. Furthermore, we extend the logic to (↓ ,) by adding the hybrid operator ↓a. and existential modality . By defining local named dynamic operators and providing recursion axioms for them, we obtain a sound and strongly complete calculus 𝖢_𝖫𝖫𝖵 for (↓ ,) . Finally, we show that for any set X of global or local operators, the calculus 𝖢_𝖦𝖫𝖵(X) and 𝖢_𝖫𝖫𝖵(X) are still sound and strongly complete w.r.t the logic (X) and (↓ ,,X) , respectively.
Taking an intuitionistic stance and regarding proof theory as methodologically basic for semantics and logic, we develop, building on previous work (J. Log. Comput. 31(3): 704-770, 2021; Bull. Symb. Log. 32(1): 136-196, 2026), a proof-theoretic framework for the study of the inferential interaction between counterfactuals and belief/knowledge. Relying on the technical results obtained for this framework (preservation, normalization, the subexpression property), we give a proof-theoretic semantics for elementary constructions which combine (counter)factuals, belief, knowledge, disbelief, and ignorance.
Debugging an ontology stated in description logic is a cognitively straining task for humans and there has been a recent increase in literature discussing various methods of facilitating this task. While some of these methods involve selected fragments of cognitive theory, none systematically integrate a cognitive theory. This paper aims to fill that gap by using the cognitive architecture ACT-R to model the ABox consistency task; a task which is essential for debugging ontologies. The resulting model is called SHARP (Simulating Human ABox Reasoning Performance) which simulates the ABox consistency algorithm as if it were run by a human mind. We evaluate the model by comparing its predicted inference times with empirical data gathered from an experiment with 70 participants. The complexity measures based on SHARP prove very accurate in predicting the complexity ordering of the set of ABoxes used in the experiment and outperform other measures found in the literature. These measures can thus be considered cognitively adequate, which opens up opportunities for them being utilised in cognitively optimised debugging of ontologies. Besides the complexity ordering, several other hypotheses are tested, which demonstrate that SHARP displays certain inaccurate consequences on a finer scale. These are considered points of improvement.
Recently, Bandaru et al. and Borumand Saeid et al. introduced transitive GE-algebras (for short, TGE-algebras) and antisymmetric transitive GE-algebras (for short, ATGE-algebras), respectively. In this paper, we present TGE-logic, the corresponding logic to these algebras. We show that the variety of TGE-algebras forms an algebraic semantics for TGE-logic in the sense of (Blok Pigozzi, 1989). Furthermore, we prove that TGE-logic is strongly sound and complete with respect to TGE-algebras. We demonstrate that the equivalent algebraic semantics for TGE-logic is the variety of ATGE-algebras and that TGE-logic is algebraizable in the sense of (Blok Pigozzi, 1989). Moreover, we prove that TGE-logic is strongly sound and complete with respect to ATGE-algebras. We further prove each congruence relation θ on an ATGE-algebra ℒ= (L, *, 1) is uniquely determined by the equivalence class of 1 under θ , where the quotient algebra ℒ/θ is an ATGE-algebra. Finally, we show the independence of the axioms of TGE-logic.
We design a method for solving natural language one-dimensional ordering problems by tightly integrating and co-developing a semantic parser with a logical inference module that deduces conclusions from the constraints stated in the premises. The semantic parser builds on Heim and Kratzer’s syntax-based compositional semantics with lambda calculus and introduces abstract types, templated rules, and a dynamic component for interpreting entities. It maps natural language into first-order logical forms defined in an axiom system and domain language that we develop for one-dimensional ordering problems. These forms are evaluated by a logic-based inference module that we design and develop which enforces ordering constraints and determines whether candidate statements hold in all, some, or no possible worlds consistent with the premises, while addressing difficult constructs such as partial ordering and negation. The resulting system, the Formal Semantic Logic Inferer (FSLI), tightly integrates formal semantics with logic programming to provide a linguistically principled and logically sound framework for logical deduction problems stated in natural language. We demonstrate FSLI’s effectiveness on both synthetic and exam-style problems, achieving perfect performance in the controlled setting of the synthetic problems and high performance on the more linguistically and logically demanding exam-style ones.
We present a formalism that allows to distinguish between, on the one hand, expectations about future states (agents’ a priori beliefs about those states), and, on the other hand, what will be known and believed by the different agents in those future states (a posteriori knowledge and belief). We use plausibility models within Dynamic Epistemic Logic (DEL) to model beliefs, expectations and judgments of plausibility. Having such a formalism in place, we can reason about an agent’s false beliefs and false expectations, and when to make belief updates (relevant announcements) so future undesirable situations may be avoided. A potential application of our framework is human-robot interaction. Based on reasoning about the human’s false expectation, a proactive robot can autonomously decide when and what to announce to help avoiding that the human ends up in an undesirable state.
With the emergence of large language models and their impressive performance across diverse natural language processing tasks, the question of whether connectionist models can exhibit compositionality without relying on symbolic processing has regained attention in both cognitive science and artificial intelligence. However, interpretability challenges faced by neural networks make it difficult to determine whether they genuinely generalize compositional structures. In this paper, we introduce a targeted evaluation framework designed to directly assess the ability of transformer-based language models to translate natural language sentences into first-order logic expressions, a task that requires both nuanced linguistic understanding and compositional generalization. To demonstrate our framework, we fine-tune two different sizes of the T5 language model using our dataset, evaluating their performance through three experiments that employ four task-specific evaluation metrics. Our findings reveal that while these models achieve high scores on test data sharing the logical and structural complexity of the training set, their performance drops markedly as sentence length, the number of truth-functional connectives and predicates, and the depth of hierarchical composition increase. More strikingly, the models fail to generalize even when complexity increases solely through repeated applications of a single truth-functional connective.
This paper is an investigation of variable binding as it occurs in dynamic predicate logic (DPL) as opposed to classical predicate logic (CPL). We begin by addressing a troubling conceptual problem, namely that the established notion of syntactic dynamic binding does not correspond to any well-defined notion of semantic dynamic binding. We solve this problem by conservatively re-engineering Groenendijk and Stokhof’s (1991) original semantics for DPL in such a way that the equivalence of the ensuing notion of semantic binding with the extant notion of syntactic binding can be established. We then compare this notion of dynamic binding to its counterpart in CPL. To this end, we invoke the previously invisible syntactic structure that emerges when one refines the common syntax of CPL and DPL in such a way as to render all syntactic operations both categorematic and binary branching. This allows us to formulate a general schema describing the variable binding behaviors of both logics, the only difference consisting in the value of a schematic parameter. Since binary branching and categorematicity are necessary for a semantics whose only semantic operation is unary functional application, our analysis reveals that, in a dynamic semantics of this kind, it is not (just) quantifier phrases, but rather arbitrarily complex operators that act as variable binders. The analysis also suggests that, despite first appearances, dynamic binding is not a counterexample to the principle that operators can only bind variable occurrences that lie within their syntactic scopes.
Spatial logics are formalisms for expressing topological properties of structures based on geometrical entities and relations. In this paper we consider SLCS, the Spatial Logic for Closure Spaces, recently used for describing features of images and video frames. We equip the logic with temporal operators, and provide a linear-time semantics over finite traces. The resulting formalism allows one to state properties about geometrical entities whose attributes change over time. For the given extension, we prove the equivalence of its operational semantics with a denotational one. We then introduce a temporal extension of the tool VoxLogicA, a spatial model checker based on SLCS. The extension provides users with the possibility to analyse spatio-temporal properties of interest on image streams.
In this paper, we explore relevant deontic logics with a primitive obligation operator. We critically assess Goble’s proposals for relevant deontic logics and propose alternative minimal deontic systems. We then examine the status of the ought implies can principle. Finally, we investigate options for strong deontic logics.
We embed Halpern’s theory of actual cause into a variant of dynamic logic with assignments. We achieve this by associating dynamic logic programs to its central concepts: structural equations and interventions modifying these equations. With these programs we can reduce reasoning about causality to a model checking problem in dynamic logic.
Semantics for logics with Topic Sensitive Intentional Modal operators require a structure, often a mereology, of topics. These structures have varied from mere semi-lattices and sets of partitions of possible worlds to collections of subalgebras. We will argue that a natural representation of topic is as vectors in a vector space. This idea is motivated by the use of vector space models in large language models. There, the relation between vectors corresponds to the semantic relation between the topics of the words being modeled by the vectors. As such, we reconstruct a logic of conditional hyperintensional belief given in Özgün and Berto (2021), replacing their semi-lattice of topics with a vector space of topics. In these vector-based models, the containment relation of topics is given an intuitive reading that (unlike the semi-lattice reading) is straightforwardly compatible with a selection of modifications and extensions that we will discuss. We are offering a new semantics for a logic: the main upshots are a formal framework for topical vector spaces, and that the introduced semantics is philosophically satisfying.
This paper proposes an approach to information-based logics using many-logic modal structures (MLMS). These structures can express accessibility relations between worlds with different underlying logics by anchoring them to a base lattice, which contains the semantics of each logic as a down-complete sublattice. MLMS are suitable for representing connections between information states (i.e., configurations of databases) and the evolution of information states over time. We will illustrate the application of MLMS by means of the six-valued logic of evidence and truth LET+K , related to the lattice L6, and some four-, three-, and two-valued logics related to down-complete sublattices of L6. These logics are capable of representing paracomplete, paraconsistent, and classical contexts with six-, four-, three-, and two-valued scenarios.
The logic of analytic implication PAI developed by William T. Parry is part of a family of relevance logics that exhibits a strong variable-sharing property: ϕ→ψ is a theorem only if every variable occurring in ψ also occurs in ϕ . A demodalized version of PAI , known as DAI , was formulated in Dunn (1972). Urquhart (1973) further introduced a modal extension of DAI , called the logic of analytic implication with necessity, AIN . Urquhart conjectured that PAI can be embedded into AIN by a Gödel-McKinsey-Tarski style translation. This paper provides a proof of this previously unverified conjecture and extends the result to other logics in the neighbourhood of PAI . In particular, we show that intuitionistic PAI can be embedded into AIN by the Gödel-McKinsey-Tarski translation.
The commas between the premises in an inference from ψ _1,… ,ψ _n to φ are normally treated as conjunctions. This is fine, except when we investigate to what extent a consequence relation, or a set of inference rules, fixes the meaning of the logical constants (Carnap’s Categoricity Problem): it then in effect constitutes a bias in favor of the standard interpretation of ∧ . I look at what happens to the categoricity of some sublogics of classical propositional logic if we avoid that bias by requiring that there be exactly one premise. This binary format is also common in the literature. It turns out that intuitionistic logic loses its categoricity, whereas classical logic keeps it. I also consider Holliday’s fundamental logic, Goldblatt’s orthologic, and some other related logics.
We present a formal framework encompassing concurrency theoretic and modal logic based approaches to the modeling and verification of dynamic multi-agent systems. We develop a model of computation merging classical labeled transition systems and multi-agent Kripke frames. Based on this model, which we call a Kripke labeled transition system, we provide a modal logic and a process algebra for the specification and analysis of interacting multi-agent systems. Our logic is obtained by combining proof systems for Hennessy-Milner Logic and the normal epistemic logic _n and is sound and complete with respect to its intended models. Further, we show that this logic is decidable and induces a behavioral equivalence combining classical notions of bisimulation. We prove that our process algebra is adequate for specifying the behavior of Kripke labeled transition systems and we show its effectiveness and usability through real-world examples.
This paper examines a range of logical systems within the family of variable inclusion logics—also known as containment logics. We focus on those logics that restrict classically valid inferences to ones meeting specific variable inclusion constraints, hence called variable inclusion companions of Classical Logic. These constraints can be seen as enforcing varying degrees of relevance between premises and conclusions, placing these systems within the broader tradition of relevance logics. We review established companions of Classical Logic, including Weak Kleene logics pure variable inclusion logics, uniform Weak Kleene logics and their intersection—pure uniform logics. We then introduce two new systems named analytic and synthetic companions of Classical Logic. We characterize their consequence relations and interpret them, as their names suggest, as validating only analytic and synthetic inferences. Lastly, we argue that these systems more effectively address the irrelevance cases that motivated earlier proposals, by correctly tracing them to the Monotonicity of the consequence relation.
We develop a topical framework for implication-in-fiction by representing topics as subalgebras, following [12]. We propose an account where those propositions follow within the fiction which (1) follow tout court and (2) are on topic. This is formally modeled in an algebra of propositions as the intersection of a subalgebra and a filter, both of which are generated by the values of the premises under some interpretation of the language in the algebra. We then show how this notion generalises to a Tarskian consequence relation over classes of algebras, and show that in some cases this consequence relation satisfies the Proscriptive Principle (PP), and thus is appropriate for logics of analytic containment.
This paper investigates the logic of grounding, a non-causal explanatory relation. While the study of this field is flourishing, it is still in its early stages. This paper contributes to the literature by presenting 𝒢_LWG , a novel sequent calculus for weak full grounding. While it provides a sequent-style presentation of the existing axiomatic system LWG proposed by Adam Lovett, our calculus is balanced and avoids the ad-hoc rules contained in LWG . An important fact shown in this paper is that if a sequent Γ⇒Δ is derivable in 𝒢_LWG , then any variable occurring positively (or negatively) in Γ also occurs positively (or negatively) in Δ . This highlights a deep connection between grounding and variable inclusion. This property, in particular, suggests a similarity to Rohan French’s sequent calculus for analytic containment, 𝒢_AC . Indeed, we demonstrate that 𝒢_LWG is the negation dual of 𝒢_AC . The paper concludes by proving the equivalence between 𝒢_LWG and LWG .
