An injection structure 𝒜= (A,f) is a set A together with a one-place one-to-one function f. 𝒜 is a Finite State Transducer (abbreviated FST) injection structure if A is a regular set, that is, the set of words accepted by some finite automaton, and f is realized by a deterministic finite-state transducer. Automatic relational structures have been well-studied along with the isomorphism problem for automatic structures. For an FST injection structure (A, f), the graph of f is not necessarily automatic. We continue the study of the complexity of FST injection structures by showing that the isomorphism problem for unary FST injection structures is decidable in quadratic time in the size (number of states) of the FST.
Complex reasoning problems are most clearly and easily specified using logical rules, but require recursive rules with aggregation such as count and sum for practical applications. Unfortunately, the meaning of such rules has been a significant challenge, leading to many disagreeing semantics. This paper describes a unified semantics for recursive rules with aggregation, extending the unified founded semantics and constraint semantics for recursive rules with negation. The key idea is to support simple expression of the different assumptions underlying different semantics, and orthogonally interpret aggregation operations using their simple usual meaning. We present a formal definition of the semantics, prove important properties of the semantics and compare with prior semantics. In particular, we present an efficient inference over aggregation that gives precise answers to all examples we have studied from the literature. We also apply our semantics to a wide range of challenging examples, and show that our semantics is simple and matches the desired results in all cases. Finally, we describe experiments on the most challenging examples, exhibiting unexpectedly superior performance over well-known systems when they can compute correct answers.
We introduce the probabilistic two-agent justification logic IPJ, a logic in which we can reason about agents that perform interactive proofs. In order to study the growth rate of the probabilities in IPJ, we present a new method of parametrizing IPJ over certain negligible functions. Further, our approach leads to a new notion of zero-knowledge proofs.
Small model property is an important property that implies decidability. We show that the small model size is directly related to some important resources in games and automata for checking provability.
In this paper, we discuss exact and parameterized algorithms for the problem of finding a read-once refutation in an unsatisfiable Horn Constraint System (HCS). Recall that a linear constraint system 𝐀 · 𝐱 ≥ 𝐛 is said to be a Horn constraint system, if each entry in 𝐀 belongs to the set {0,1,-1} and at most one entry in each row of 𝐀 is positive. In this paper, we examine the importance of constraints in which more variables have negative coefficients than have positive coefficients. There exist several algorithms for checking whether a Horn constraint system is feasible. To the best of our knowledge, these algorithms are not certifying, i.e., they do not provide a certificate of infeasibility. Our work is concerned with providing a specialized class of certificates called “read-once refutations”. In a read-once refutation, each constraint defining the HCS may be used at most once in the derivation of a refutation. The problem of checking if an HCS has a read-once refutation (HCS ROR) has been shown to be NP-hard. We analyze the HCS ROR problem from two different algorithmic perspectives, viz., parameterized algorithms and exact exponential algorithms.
