相关论文: Action Logic is Undecidable

Representing time is crucial for cyber-physical systems and has been studied extensively in the Situation Calculus. The most commonly used approach represents time by adding a real-valued fluent $\mathit{time}(a)$ that attaches a time point…

This is the second paper in a series of three, where we take on the unified theory of non-Archimedean group actions, length functions and infinite words. Here, for an arbitrary group $G$ of infinite words over an ordered abelian group…

Let $\Gamma$ be an irreducible lattice of $\Q$-rank $\geq 2$ in a semisimple Lie group of noncompact type. We prove that any action of $\Gamma$ on a $\CAT(0)$ cubical complex has a global fixed point.

Formal reasoning about inductively defined relations and structures is widely recognized not only for its mathematical interest but also for its importance in computer science, and has applications in verifying properties of programs and…

We consider the bimodal language, where the first modality is interpreted by a binary relation in the standard way, and the second is interpreted by the relation of inequality. It follows from Hughes (1990), that in this language,…

Coalition logic is one of the most popular logics for multi-agent systems. While epistemic extensions of coalition logic have received much attention, existence of their complete axiomatisations has so far been an open problem. In this…

The logical method proposed by Goubault, Ledent, and Rajsbaum provides a novel way to show the unsolvability of distributed tasks by means of a logical obstruction, which is an epistemic logic formula describing the reason of unsolvability.…

First-order temporal logics are notorious for their bad computational behaviour. It is known that even the two-variable monadic fragment is highly undecidable over various linear timelines, and over branching time even one-variable…

We prove that the problems of representing a finite ordered complemented semigroup or finite lattice-ordered semigroup as an algebra of binary relations over a finite set are undecidable. In the case that complementation is taken with…

We study first-order logic (FO) over the structure consisting of finite words over some alphabet $A$, together with the (non-contiguous) subword ordering. In terms of decidability of quantifier alternation fragments, this logic is…

Metric Temporal Logic, $\mtlfull$ is amongst the most studied real-time logics. It exhibits considerable diversity in expressiveness and decidability properties based on the permitted set of modalities and the nature of time interval…

Doubts are raised concerning the usual interpretation of the alleged failure, by quantum mechanics, of the distributive law of classical logic. The difficulty raised by incompatible sets of observables is overcome within an epistemic…

Coalition Logic is primarily concerned with what coalitions can achieve, whereas what coalitions cannot achieve -- their \emph{inability} -- has received comparatively little explicit attention. This asymmetry matters in artificial…

Stalnaker and Thomason famously proved that the conditional logic \textsf{C2} with first-order quantifiers is complete with respect to a selection function semantics. However, the selection functions used in this completeness result take…

We show that the problem `whether a finite set of regular-linear axioms defines a rigid theory' is undecidable.

We study the problem of deciding satisfiability of first order logic queries over views, our aim being to delimit the boundary between the decidable and the undecidable fragments of this language. Views currently occupy a central place in…

We show that the unification problem `is there a substitution instance of a given formula that is provable in a given logic?' is undecidable for basic modal logics K and K4 extended with the universal modality. It follows that the…

The recently initiated approach called computability logic is a formal theory of interactive computation. See a comprehensive online source on the subject at http://www.cis.upenn.edu/~giorgi/cl.html . The present paper contains a soundness…

We extend the epistemic logic with De Morgan negation by Fagin et al. (Artif. Intell. 79, 203-240, 1995) by adding operators for universal and common knowledge in a group of agents, and with a formalization of information update using a…

We show that a large class of divisible abelian $\ell$-groups (lattice ordered groups) of continuous functions is interpretable (in a certain sense) in the lattice of the zero sets of these functions. This has various applications to the…