计算机科学中的逻辑

We give a new, direct proof of the tetrachotomy classification for the model-checking problem of positive equality-free logic parameterised by the model. The four complexity classes are Logspace, NP-complete, co-NP-complete and…

Mathematical optimization is ubiquitous in modern applications. However, in practice, we often need to use nonlinear optimization models, for which the existing optimization tools such as Cplex or Gurobi may not be directly applicable and…

Mathematical analysis of the analytic hierarchy process (AHP) led to the development of a mathematical function, usually called the inconsistency index, which has the center role in measuring the inconsistency of the judgements in AHP.…

In 1864 W.S.B. Woolhouse formulated the Cotton-Spinning problem. This problem boils down to the following. A piecer works at a spinning mule and walks back and forth to repair broken threads. The question is how far the piecer is expected…

We study the time complexity of the weighted first-order model counting (WFOMC) over the logical language with two variables and counting quantifiers. The problem is known to be solvable in time polynomial in the domain size. However, the…

Epistemic and doxastic logics are modal logics for knowledge and belief, and serve as foundational models for rational agents in game theory, philosophy, and computer science. We examine the consequences of modeling agents capable of a…

Session types are a typed approach to message-passing concurrency, where types describe sequences of intended exchanges over channels. Session type systems have been given strong logical foundations via Curry-Howard correspondences with…

First-order logic has been established as an important tool for modeling and verifying intricate systems such as distributed protocols and concurrent systems. These systems are parametric in the number of nodes in the network or the number…

Motivated by the search for forms of distributed belief that do not collapse in the face of conflicting information, this paper introduces the notions of cautious and bold distributed belief. Both notions rely on maximally consistent…

This paper provides an adaptation of branching bisimilarity to reactive systems with time-outs. Multiple equivalent definitions are procured, along with a modal characterisation and a proof of its congruence property for a standard process…

This paper proposes a new methodology for early validation of high-level requirements on cyber-physical systems with the aim of improving their quality and, thus, lowering chances of specification errors propagating into later stages of…

In multiagent systems autonomous agents interact with each other to achieve individual and collective goals. Typical interactions concern negotiation and agreement on resource exchanges. Modeling and formalizing these agreements pose…

Finitely many two-way automata work independently and synchronously on a unary input. Some of their states are broadcasting, i.e., dispatched to all other automata. At each step of the computation, each automaton changes state and moves…

This paper lays a practical foundation for using abstract interpretation with an abstract domain that consists of sets of quantified first-order logic formulas. This abstract domain seems infeasible at first sight due to the complexity of…

In this report, we study partial quantifier elimination (PQE) for propositional CNF formulas. PQE is a generalization of quantifier elimination where one can limit the set of clauses taken out of the scope of quantifiers to a small subset…

We present a novel automata-based approach to address linear temporal logic modulo theory (LTL-MT) as a specification language for data words. LTL-MT extends LTL_f by replacing atomic propositions with quantifier-free multi-sorted…

Standpoint linear temporal logic SLTL is a recent formalism able to model possibly conflicting commitments made by distinct agents, taking into account aspects of temporal reasoning. In this paper, we analyse the computational properties of…

We show a projective Beth definability theorem for logic programs under the stable model semantics: For given programs $P$ and $Q$ and vocabulary $V$ (set of predicates) the existence of a program $R$ in $V$ such that $P \cup R$ and $P \cup…

Several paradigms for declarative problem solving start from a specification in a high-level language, which is then transformed to a low-level language, such as SAT or SMT. Often, this transformation includes a "grounding" step to remove…

This thesis embarks on a comprehensive exploration of formal computational models that underlie typed programming languages. We focus on programming calculi, both functional (sequential) and concurrent, as they provide a compelling rigorous…