Search results for "Logic in computer science"
showing 10 items of 129 documents
Logical and pseudo-logical optical fibre networks based on two-state (binary) optical fibre sensors for industrial monitoring and control systems
2005
The possibilities of development of logical and pseudo-logical optical fibre networks for monitoring and control of equipment and industrial sites are presented. Such networks composed of simple binary attenuation and optical fibre communication lines may also be used as fast and reliable systems developing a final command signal - logical and/or pseudo-logical, depending or the architecture of network and the type of located sensors. They realise the process similar to standard electronic logical sets but use the optical signal directly on the monitored or controlled device. The analysis of serial and parallel networks was carried out in the "dark" mode detection. The examples of networks …
Unit contradiction versus unit propagation
2012
Some aspects of the result of applying unit resolution on a CNF formula can be formalized as functions with domain a set of partial truth assignments. We are interested in two ways for computing such functions, depending on whether the result is the production of the empty clause or the assignment of a variable with a given truth value. We show that these two models can compute the same functions with formulae of polynomially related sizes, and we explain how this result is related to the CNF encoding of Boolean constraints.
Alternating, private alternating, and quantum alternating realtime automata
2014
We present new results on realtime alternating, private alternating, and quantum alternating automaton models. Firstly, we show that the emptiness problem for alternating one-counter automata on unary alphabets is undecidable. Then, we present two equivalent definitions of realtime private alternating finite automata (PAFAs). We show that the emptiness problem is undecidable for PAFAs. Furthermore, PAFAs can recognize some nonregular unary languages, including the unary squares language, which seems to be difficult even for some classical counter automata with two-way input. Regarding quantum finite automata (QFAs), we show that the emptiness problem is undecidable both for universal QFAs o…
Zero-Error Affine, Unitary, and Probabilistic OBDDs
2017
We introduce the affine OBDD model and show that zero-error affine OBDDs can be exponentially narrower than bounded-error unitary and probabilistic OBDDs on certain problems. Moreover, we show that Las Vegas unitary and probabilistic OBDDs can be quadratically narrower than deterministic OBDDs. We also obtain the same results by considering the automata versions of these models.
Reordering Method and Hierarchies for Quantum and Classical Ordered Binary Decision Diagrams
2017
We consider Quantum OBDD model. It is restricted version of read-once Quantum Branching Programs, with respect to "width" complexity. It is known that maximal complexity gap between deterministic and quantum model is exponential. But there are few examples of such functions. We present method (called "reordering"), which allows to build Boolean function $g$ from Boolean Function $f$, such that if for $f$ we have gap between quantum and deterministic OBDD complexity for natural order of variables, then we have almost the same gap for function $g$, but for any order. Using it we construct the total function $REQ$ which deterministic OBDD complexity is $2^{\Omega(n/\log n)}$ and present quantu…
Inductive types in homotopy type theory
2012
Homotopy type theory is an interpretation of Martin-L\"of's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof s…
Transitive reasoning with imprecise probabilities
2015
We study probabilistically informative (weak) versions of transitivity, by using suitable definitions of defaults and negated defaults, in the setting of coherence and imprecise probabilities. We represent p-consistent sequences of defaults and/or negated defaults by g-coherent imprecise probability assessments on the respective sequences of conditional events. Finally, we prove the coherent probability propagation rules for Weak Transitivity and the validity of selected inference patterns by proving the p-entailment for the associated knowledge bases.
Topological Logics with Connectedness over Euclidean Spaces
2013
We consider the quantifier-free languages, Bc and Bc °, obtained by augmenting the signature of Boolean algebras with a unary predicate representing, respectively, the property of being connected, and the property of having a connected interior. These languages are interpreted over the regular closed sets of R n ( n ≥ 2) and, additionally, over the regular closed semilinear sets of R n . The resulting logics are examples of formalisms that have recently been proposed in the Artificial Intelligence literature under the rubric Qualitative Spatial Reasoning. We prove that the satisfiability problem for Bc is undecidable over the regular closed semilinear sets in all dimensions greater than 1,…
Functions definable by numerical set-expressions
2011
A "numerical set-expression" is a term specifying a cascade of arithmetic and logical operations to be performed on sets of non-negative integers. If these operations are confined to the usual Boolean operations together with the result of lifting addition to the level of sets, we speak of "additive circuits". If they are confined to the usual Boolean operations together with the result of lifting addition and multiplication to the level of sets, we speak of "arithmetic circuits". In this paper, we investigate the definability of sets and functions by means of additive and arithmetic circuits, occasionally augmented with additional operations.
Sequentializing Parameterized Programs
2012
We exhibit assertion-preserving (reachability preserving) transformations from parameterized concurrent shared-memory programs, under a k-round scheduling of processes, to sequential programs. The salient feature of the sequential program is that it tracks the local variables of only one thread at any point, and uses only O(k) copies of shared variables (it does not use extra counters, not even one counter to keep track of the number of threads). Sequentialization is achieved using the concept of a linear interface that captures the effect an unbounded block of processes have on the shared state in a k-round schedule. Our transformation utilizes linear interfaces to sequentialize the progra…