Search results for "Computer Science::Logic in Computer Science"
showing 10 items of 72 documents
On Finite Satisfiability of Two-Variable First-Order Logic with Equivalence Relations
2009
We show that every finitely satisfiable two-variable first-order formula with two equivalence relations has a model of size at most triply exponential with respect to its length. Thus the finite satisfiability problem for two-variable logic over the class of structures with two equivalence relations is decidable in nondeterministic triply exponential time. We also show that replacing one of the equivalence relations in the considered class of structures by a relation which is only required to be transitive leads to undecidability. This sharpens the earlier result that two-variable logic is undecidable over the class of structures with two transitive relations.
Logics and operators
2003
Two connectives are of special interest in metalogical investigations — the connective of implication which is important due to its connections to the notion of inference, and the connective of equivalence. The latter connective expresses, in the material sense, the fact that two sentences have the same logical value while in the strict sense it expresses the fact that two sentences are interderivable on the basis of a given logic. The process of identification of equivalent sentences relative to theories of a logic C defines a class of abstract algebras. The members of the class are called Lindenbaum-Tarski algebras of the logic C. One may abstract from the origin of these algebras and exa…
Vector description of higher-order modes in photonic crystal fibers
2000
We extensively study the propagation features of higher-order modes in a photonic crystal fiber (PCF). Our analysis is based on a full-vector modal technique specially adapted to accurately describe light propagation in PCF's. Unlike conventional fibers, PCF's exhibit a somewhat unusual mechanism for the generation of higher-order modes. Accordingly, PCF's are characterized by the constancy of the number of modes below a wavelength threshold. An explicit verification of this property is given through a complete analysis of the dispersion relations of higher-order modes in terms of the structural parameters of this kind of fiber. The transverse irradiance distributions for some of these high…
Monads in double categories
2010
We extend the basic concepts of Street's formal theory of monads from the setting of 2-categories to that of double categories. In particular, we introduce the double category Mnd(C) of monads in a double category C and define what it means for a double category to admit the construction of free monads. Our main theorem shows that, under some mild conditions, a double category that is a framed bicategory admits the construction of free monads if its horizontal 2-category does. We apply this result to obtain double adjunctions which extend the adjunction between graphs and categories and the adjunction between polynomial endofunctors and polynomial monads.
The Crane Beach Conjecture
2002
A language L over an alphabet A is said to have a neutral letter if there is a letter e/spl isin/A such that inserting or deleting e's from any word in A* does not change its membership (or non-membership) in L. The presence of a neutral letter affects the definability of a language in first-order logic. It was conjectured that it renders all numerical predicates apart from the order predicate useless, i.e., that if a language L with a neutral letter is not definable in first-order logic with linear order then it is not definable in first-order. Logic with any set /spl Nscr/ of numerical predicates. We investigate this conjecture in detail, showing that it fails already for /spl Nscr/={+, *…
Monadic second-order logic over pictures and recognizability by tiling systems
1994
We show that a set of pictures (rectangular arrays of symbols) is recognized by a finite tiling system if and only if it is definable in existential monadic second-order logic. As a consequence, finite tiling systems constitute a notion of recognizability over two-dimensional inputs which at the same time generalizes finite-state recognizability over strings and matches a natural logic. The proof is based on the Ehrenfeucht-FraIsse technique for first-order logic and an implementation of “threshold counting” within tiling systems.
Monadic Second-Order Logic over Rectangular Pictures and Recognizability by Tiling Systems
1996
Abstract It is shown that a set of pictures (rectangular arrays of symbols) is recognized by a finite tiling system iff it is definable in existential monadic second-order logic. As a consequence, finite tiling systems constitute a notion of recognizability over two-dimensional inputs which at the same time generalizes finite-state recognizability over strings and also matches a natural logic. The proof is based on the Ehrenfeucht–Fraisse technique for first-order logic and an implementation of “threshold counting” within tiling systems.
Basic Properties of Quasivarieties
2015
This chapter supplies basic facts concerning quasivarieties and the equational systems associated with quasivarieties. Many of these facts are of syntactical character. An equational logic is an extension of the familiar Birkhoff’s logic. The narrative structure of the book is strictly linked with the properties of lattices of theories of equational logics. Examining these lattice requires formal tools. They are introduced in this part; some of them are new.
Protoalgebraicity and the Deduction Theorem
2001
This chapter is intended as an introduction to the Deduction Theorem and to applications of this theorem in metalogic.
Quantum Finite State Transducers
2000
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.