Search results for "Logic in computer science"
showing 10 items of 129 documents
The generalised type-theoretic interpretation of constructive set theory
2006
We present a generalisation of the type-theoretic interpretation of constructive set theory into Martin-Löf type theory. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive instead of being formulated via the propositions-as-types representation. The original interpretation treated logic in Martin-Löf type theory via the propositions-as-types interpretation. The generalisation involves replacing Martin-Löf type theory with a new type theory in which logic is treated as primitive. The primitive treatment of logic in type theories allows us to study reinterpretations of logic, such as the double-negation translation.
Logics with counting and equivalence
2014
We consider the two-variable fragment of first-order logic with counting, subject to the stipulation that a single distinguished binary predicate be interpreted as an equivalence. We show that the satisfiability and finite satisfiability problems for this logic are both NEXPTIME-complete. We further show that the corresponding problems for two-variable first-order logic with counting and two equivalences are both undecidable.
Quantum Finite State Transducers
2001
We introduce quantum finite state transducers (qfst), and study the class of relations which they compute. It turns out that they share many features with probabilistic finite state transducers, especially regarding undecidability of emptiness (at least for low probability of success). However, like their 'little brothers', the quantum finite automata, the power of qfst is incomparable to that of their probabilistic counterpart. This we show by discussing a number of characteristic examples.
Error-Free Affine, Unitary, and Probabilistic OBDDs
2018
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 for the automata versions of these models.
Error-Free Affine, Unitary, and Probabilistic OBDDs
2021
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 for the automata counterparts of these models.
The monadic quantifier alternation hierarchy over grids and pictures
1998
The subject of this paper is the expressive power of monadic second-order logic over two-dimensional grids. We give a new, self-contained game-theoretical proof of the nonexpressibility results of Matz and Thomas. As we show, this implies the strictness of the monadic second-order quantifier alternation hierarchy over grids.
Probabilistic Interpretations of Predicates
2016
In classical logic, any m-ary predicate is interpreted as an m-argument two-valued relation defined on a non-empty universe. In probability theory, m-ary predicates are interpreted as probability measures on the mth power of a probability space. m-ary probabilistic predicates are equivalently semantically characterized as m-dimensional cumulative distribution functions defined on \(\mathbb {R}^m\). The paper is mainly concerned with probabilistic interpretations of unary predicates in the algebra of cumulative distribution functions defined on \(\mathbb {R}\). This algebra, enriched with two constants, forms a bounded De Morgan algebra. Two logical systems based on the algebra of cumulative…
Graph Connectivity, Monadic NP and built-in relations of moderate degree
1995
It has been conjectured [FSV93] that an existential secondoder formula, in which the second-order quantification is restricted to unary relations (i.e. a Monadic NP formula), cannot express Graph Connectivity even in the presence of arbitrary built-in relations.
Finitary Representations and Images of Transitive Finitary Permutation Groups
1999
Abstract We characterize the point stabilizers and kernels of finitary permutation representations of infinite transitive groups of finitary permutations. Moreover, the number of such representations is determined.
Transforming XML documents to OWL ontologies: A survey
2015
The aims of XML data conversion to ontologies are the indexing, integration and enrichment of existing ontologies with knowledge acquired from these sources. The contribution of this paper consists in providing a classification of the approaches used for the conversion of XML documents into OWL ontologies. This classification underlines the usage profile of each conversion method, providing a clear description of the advantages and drawbacks belonging to each method. Hence, this paper focuses on two main processes, which are ontology enrichment and ontology population using XML data. Ontology enrichment is related to the schema of the ontology (TBox), and ontology population is related to …