Varieties of topological quasi-Boolean algebras in the vicinity of pre-rough algebras [28, 29] are expanded to residuated algebraic structures by introducing a new implication operation and its residual in these structures. Sequent calculi for some classes of residuated algebraic structures are established. These sequent calculi have the strong finite model property which yields the decidability of the word problem for corresponding classes of algebraic structures.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
We prove that there are single Henkin quantifiers such that first order logic augmented by one of these quantifiers is undecidable in the empty vocabulary. We estimate the size of such quantifiers proving undecidability of Lø(H12) and Lø(E10).
3
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this paper we show that subsumption problems in lightweight description logics (such as εL and εL+) can be expressed as uniform word problems in classes of semilattices with monotone operators. We use possibilities of efficient local reasoning in such classes of algebras, to obtain uniform PTIME decision procedures for CBox subsumption in εL, εL+ and extensions thereof. These locality considerations allow us to present a new family of (possibly many-sorted) logics which extend εL and εL+ with n-ary roles and/or numerical domains. As a by-product, this allows us to show that the algebraic models of εL and εL+ have ground interpolation and thus that εL, εL+, and their extensions studied in this paper have interpolation.
4
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
Using 1947 work of Post showing that the word problem for semigroups is unsolvable, we explicitly exhibit an algebraic characterization of the bits of the halting probability W. Our proof closely follows a 1978 formulation of Post's work by M. Davis. The proof is self-contained and not very complicated.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.