计算机科学中的逻辑

Logic can define how agents are provided or denied access to resources, how to interlink resources using mining processes and provide users with choices for possible next steps in a workflow. These decisions are for the most part hidden,…

We give a new proof of a theorem of Mints that the positive fragment of minimal predicate logic is decidable. The idea of the proof is to replace the eigenvariable condition of sequent calculus by an appropriate scoping mechanism. The…

We extend the notion of Heyting algebra to a notion of truth values algebra and prove that a theory is consistent if and only if it has a B-valued model for some non trivial truth values algebra B. A theory that has a B-valued model for all…

An operation is called covert if it conceals the identity of the actor; it is called clandestine if the very fact that the operation is conducted is concealed. The paper proposes a formal semantics of clandestine operations and introduces a…

We propose Teamwork Synthesis, a version of the distributed synthesis problem with application to teamwork multi-agent systems. We reformulate the distributed synthesis question by dropping the fixed interaction architecture among agents as…

This technical report investigates Kripke-style modal type theories, both simply typed and dependently typed. We examine basic meta-theories of the type theories, develop their substitution calculi, and give normalization by evaluation…

The rewriting system sigma is the set of rules propagating explicit substitutions in the lambda-calculus with explicit substitutions. In this note, we prove the undecidability of unification modulo sigma.

We study the complexity of reductions for weighted reachability in parametric Markov decision processes. That is, we say a state p is never worse than q if for all valuations of the polynomial indeterminates it is the case that the maximal…

Logical frameworks provide natural and direct ways of specifying and reasoning within deductive systems. The logical framework LF and subsequent developments focus on finitary proof systems, making the formalization of circular proof…

Metatheorems about type theories are often proven by interpreting the syntax into models constructed using categorical gluing. We propose to use only sconing (gluing along a global section functor) instead of general gluing. The sconing is…

Quantitative notions of bisimulation are well-known tools for the minimization of dynamical models such as Markov chains and ordinary differential equations (ODEs). In \emph{forward bisimulations}, each state in the quotient model…

Ternary logic is expected to increase the area efficiency of VLSI due to its expressiveness compared to the traditional binary logic. This paper proposes a new symmetric ternary logic and a systematic logic composition methodology that…

We present a first-order linear-time temporal logic for reasoning about the evolution of directed graphs. Its semantics is based on the counterpart paradigm, thus allowing our logic to represent the creation, duplication, merging, and…

We report on intermediate results of -- to the best of our knowledge -- the first study of completeness thresholds for (partially) bounded memory safety proofs. Specifically, we consider heap-manipulating programs that iterate over arrays…

Many applications of graph transformation require rules that change a graph without introducing new consistency violations. When designing such rules, it is natural to think about the desired outcome state, i.e., the desired effect, rather…

Peter Andrews has proposed, in 1971, the problem of finding an analog of the Skolem theorem for Simple Type Theory. A first idea lead to a naive rule that worked only for Simple Type Theory with the axiom of choice and the general case has…

In reverse engineering of database queries, we aim to construct a query from a given set of answers and non-answers; it can then be used to explore the data further or as an explanation of the answers and non-answers. We investigate this…

Call-by-Push-Value (CBPV) is a programming paradigm subsuming both Callby-Name (CBN) and Call-by-Value (CBV) semantics. The essence of this paradigm is captured by the Bang Calculus, a (concise) term language connecting CBPV and Linear…

We make two contributions to the study of theory combination in satisfiability modulo theories. The first is a table of examples for the combinations of the most common model-theoretic properties in theory combination, namely stable…

We compare the values associated with (traditional) community based proof verification to those associated with computer proof verification. We propose ways that computer proofs might incorporate successful strategies from human…