Search results for "DF"
showing 10 items of 1699 documents
Finite Model Reasoning in Expressive Fragments of First-Order Logic
2017
Over the past two decades several fragments of first-order logic have been identified and shown to have good computational and algorithmic properties, to a great extent as a result of appropriately describing the image of the standard translation of modal logic to first-order logic. This applies most notably to the guarded fragment, where quantifiers are appropriately relativized by atoms, and the fragment defined by restricting the number of variables to two. The aim of this talk is to review recent work concerning these fragments and their popular extensions. When presenting the material special attention is given to decision procedures for the finite satisfiability problems, as many of t…
Subsumption-driven clause learning with DPLL+restarts
2019
We propose to use a DPLL+restart to solve SAT instances by successive simplifications based on the production of clauses that subsume the initial clauses. We show that this approach allows the refutation of pebbling formulae in polynomial time and linear space, as effectively as with a CDCL solver.
Adding Path-Functional Dependencies to the Guarded Two-Variable Fragment with Counting
2017
The satisfiability and finite satisfiability problems for the two-variable guarded fragment of first-order logic with counting quantifiers, a database, and path-functional dependencies are both ExpTime-complete.
Massively Parallel and Asynchronous Tsetlin Machine Architecture Supporting Almost Constant-Time Scaling
2020
Using logical clauses to represent patterns, Tsetlin Machines (TMs) have recently obtained competitive performance in terms of accuracy, memory footprint, energy, and learning speed on several benchmarks. Each TM clause votes for or against a particular class, with classification resolved using a majority vote. While the evaluation of clauses is fast, being based on binary operators, the voting makes it necessary to synchronize the clause evaluation, impeding parallelization. In this paper, we propose a novel scheme for desynchronizing the evaluation of clauses, eliminating the voting bottleneck. In brief, every clause runs in its own thread for massive native parallelism. For each training…
Visibly pushdown modular games,
2014
Games on recursive game graphs can be used to reason about the control flow of sequential programs with recursion. In games over recursive game graphs, the most natural notion of strategy is the modular strategy, i.e., a strategy that is local to a module and is oblivious to previous module invocations, and thus does not depend on the context of invocation. In this work, we study for the first time modular strategies with respect to winning conditions that can be expressed by a pushdown automaton. We show that such games are undecidable in general, and become decidable for visibly pushdown automata specifications. Our solution relies on a reduction to modular games with finite-state automat…
Computational Limitations of Affine Automata
2019
We present two new results on the computational limitations of affine automata. First, we show that the computation of bounded-error rational-values affine automata is simulated in logarithmic space. Second, we give an impossibility result for algebraic-valued affine automata. As a result, we identify some unary languages (in logarithmic space) that are not recognized by algebraic-valued affine automata with cutpoints.
New Results on Vector and Homing Vector Automata
2019
We present several new results and connections between various extensions of finite automata through the study of vector automata and homing vector automata. We show that homing vector automata outperform extended finite automata when both are defined over $ 2 \times 2 $ integer matrices. We study the string separation problem for vector automata and demonstrate that generalized finite automata with rational entries can separate any pair of strings using only two states. Investigating stateless homing vector automata, we prove that a language is recognized by stateless blind deterministic real-time version of finite automata with multiplication iff it is commutative and its Parikh image is …
Classical automata on promise problems
2015
Promise problems were mainly studied in quantum automata theory. Here we focus on state complexity of classical automata for promise problems. First, it was known that there is a family of unary promise problems solvable by quantum automata by using a single qubit, but the number of states required by corresponding one-way deterministic automata cannot be bounded by a constant. For this family, we show that even two-way nondeterminism does not help to save a single state. By comparing this with the corresponding state complexity of alternating machines, we then get a tight exponential gap between two-way nondeterministic and one-way alternating automata solving unary promise problems. Secon…
Quantum finite multitape automata
1999
Quantum finite automata were introduced by C.Moore, J.P. Crutchfield, and by A.Kondacs and J.Watrous. This notion is not a generalization of the deterministic finite automata. Moreover, it was proved that not all regular languages can be recognized by quantum finite automata. A.Ambainis and R.Freivalds proved that for some languages quantum finite automata may be exponentially more concise rather than both deterministic and probabilistic finite automata. In this paper we introduce the notion of quantum finite multitape automata and prove that there is a language recognized by a quantum finite automaton but not by a deterministic or probabilistic finite automata. This is the first result on …
The minimal probabilistic and quantum finite automata recognizing uncountably many languages with fixed cutpoints
2019
Discrete Mathematics & Theoretical Computer Science ; vol. 22 no. 1 ; Automata, Logic and Semantics ; 1365-8050