Related papers: A logic with temporally accessible iteration
In this paper, we propose a novel one-pass and tree-shaped tableau method for Timed Propositional Temporal Logic and for a bounded variant of its extension with past operators. Timed Propositional Temporal Logic (TPTL) is a real-time…
Inquisitive team logic is a variant of inquisitive logic interpreted in team semantics, which has been argued to provide a natural setting for the regimentation of dependence claims. With respect to sentences, this logic is known to be…
We introduce an extension of fixed-point logic ($\mathsf{FP}$) with a group-order operator ($\mathsf{ord}$), that computes the size of a group generated by a definable set of permutations. This operation is a generalization of the rank…
Approximation Fixpoint Theory (AFT) is a powerful theory covering various semantics of non-monotonic reasoning formalisms in knowledge representation such as Logic Programming and Answer Set Programming. Many semantics of such non-monotonic…
Regular cost functions have been introduced recently as an extension to the notion of regular languages with counting capabilities, which retains strong closure, equivalence, and decidability properties. The specificity of cost functions is…
This paper studies Linear Temporal Logic over Finite Traces (LTLf) where proposition letters are replaced with first-order formulas interpreted over arbitrary theories, in the spirit of Satisfiability Modulo Theories. The resulting logic,…
Local fixpoint iteration describes a technique that restricts fixpoint iteration in function spaces to needed arguments only. It has been studied well for first-order functions in abstract interpretation and also in model checking. Here we…
Many complex scenarios require the coordination of agents possessing unique points of view and distinct semantic commitments. In response, standpoint logic (SL) was introduced in the context of knowledge integration, allowing one to reason…
Mixed integer linear programming (MILP) is a powerful representation often used to formulate decision-making problems under uncertainty. However, it lacks a natural mechanism to reason about objects, classes of objects, and relations.…
In the last years, the adoption of active systems has increased in many fields of computer science, such as databases, sensor networks, and software engineering. These systems are able to automatically react to events, by collecting…
We show that descriptive complexity's result extends in High Order Logic to capture the expressivity of Turing Machine which have a finite number of alternation and whose time or space is bounded by a finite tower of exponential. Hence we…
This paper proposes the meeting of fuzzy logic with paraconsistency in a very precise and foundational way. Specifically, in this paper we introduce expansions of the fuzzy logic MTL by means of primitive operators for consistency and…
Recently, a novel fixed point operation has been introduced over certain non-monotonic functions between stratified complete lattices and used to give semantics to logic programs with negation and boolean context-free grammars. We prove…
Writing temporal logic formulae for properties that combine instantaneous events with overlapping temporal phenomena of some duration is difficult in classical temporal logics. To address this issue, in previous work we introduced a new…
We study the expressivity and the complexity of various logics in probabilistic team semantics with the Boolean negation. In particular, we study the extension of probabilistic independence logic with the Boolean negation, and a recently…
Formal properties represent a cornerstone of the system-correctness proofs based on formal verification techniques such as model checking. Formalizing requirements into temporal properties may be very complex and error prone, due not only…
In temporal logics, a central question is about the choice of modalities and their relative expressive power, in comparison to the complexity of decision problems such as satisfiability. In this tutorial, we will illustrate the study of…
Autonomous agents often operate in scenarios where the state is partially observed. In addition to maximizing their cumulative reward, agents must execute complex tasks with rich temporal and logical structures. These tasks can be expressed…
We consider the family of guarded and unguarded ordered logics, that constitute a recently rediscovered family of decidable fragments of first-order logic (FO), in which the order of quantification of variables coincides with the order in…
A number of extensions exist for Alternating-time Temporal Logic; some of these mix strategies and partial observability but, to the best of our knowledge, no work provides a unified framework for strategies, partial observability and…