Let M = (A, ) where (A, denotes a finite sequence of monadic predicates on A. We show that if A contains an interval of order type omega or -omega, and the monadic second-order theory of M is decidable, then there ex...
详细信息
ISBN:
(纸本)9783642150241
Let M = (A, <, <(P)over bar>) where (A, <) is a linear ordering and <(P)over bar> denotes a finite sequence of monadic predicates on A. We show that if A contains an interval of order type omega or -omega, and the monadic second-order theory of M is decidable, then there exists a non-trivial expansion M' of M by a monadic predicate such that the monadic second-order theory of M' is still decidable.
In this case study we describe an approach to a general logical framework for tracking evidence within epistemic contexts. We consider as basic an example which features two justifications for a true statement, one wh...
详细信息
ISBN:
(纸本)9783642150241
In this case study we describe an approach to a general logical framework for tracking evidence within epistemic contexts. We consider as basic an example which features two justifications for a true statement, one which is correct and one which is not. We formalize this example in a system of Justification logic with two knowers: the object agent and the observer, and we show that whereas the object agent does not logically distinguish between factive and non-factive justifications, such distinctions can be attained at the observer level by analyzing the structure of evidence terms. Basic logic properties of the corresponding two-agent Justification logic system have been established, which include Kripke-Fitting completeness. We also argue that a similar evidence-tracking approach can be applied to analyzing paraconsistent systems.
When one views (multi-sorted) existential fixed-point logic (EFPL) as a database query language, it is natural to extend it by allowing universal quantification over certain sorts. These would be the sorts for which o...
详细信息
ISBN:
(纸本)9783642150241
When one views (multi-sorted) existential fixed-point logic (EFPL) as a database query language, it is natural to extend it by allowing universal quantification over certain sorts. These would be the sorts for which one has the "closed-world" information that all entities of that sort in the real world are represented in the database. We investigate the circumstances under which this extension of EFPL retains various pleasant properties. We pay particular attention to the pleasant property of preservation by the inverse-image parts of geometric morphisms of topoi, because, as we show, this preservation property implies many of the other pleasant properties of EFPL.
This Festschrift is published in honor of Yuri Gurevich's 75th birthday. Yuri Gurevich has made fundamental contributions on the broad spectrum of logic and computerscience, including decision procedures, the mon...
详细信息
ISBN:
(数字)9783319235349
ISBN:
(纸本)9783319235332
This Festschrift is published in honor of Yuri Gurevich's 75th birthday. Yuri Gurevich has made fundamental contributions on the broad spectrum of logic and computerscience, including decision procedures, the monadic theory of order, abstract state machines, formal methods, foundations of computerscience, security, and much more. Many of these areas are reflected in the 20 articles in this Festschrift and in the presentations at the "yurifest" symposium, which was held in Berlin, Germany, on September 11 and 12, 2015. The yurifestsymposium was co-located with the 24th EACSL Annual Conference on computersciencelogic (CSL 2015).
This paper is a contribution to natural logic, the study of logical systems for linguistic reasoning. We construct a system with the following properties: its syntax is closer to that of a natural language than is fir...
详细信息
ISBN:
(纸本)9783642150241
This paper is a contribution to natural logic, the study of logical systems for linguistic reasoning. We construct a system with the following properties: its syntax is closer to that of a natural language than is first-order logic;it can faithfully represent simple sentences with standard quantifiers, subject relative clauses (a recursive construct), and negation on nouns and verbs. We also give a proof system which is complete and has the finite model property. We go further by adding comparative adjective phrases, assuming interpretations by transitive relations. This last system has all the previously-mentioned properties as well. The paper was written for theoretical computer scientists and logicians interested in areas such as decidability questions for fragments of first-order logic, modal logic, and natural deduction.
The standard translation of existential fixed-point formulas into second-order logic produces strict universal formulas, that is, formulas consisting of universal quantifiers on relations (not functions) followed by a...
详细信息
ISBN:
(纸本)9783319235349;9783319235332
The standard translation of existential fixed-point formulas into second-order logic produces strict universal formulas, that is, formulas consisting of universal quantifiers on relations (not functions) followed by an existential first-order formula. This form implies many of the pleasant properties of existential fixed-point logic, but not all. In particular, strict universal sentences can express some co-NP-complete properties of structures, whereas properties expressible by existential fixed-point formulas are always in P. We therefore investigate what additional syntactic properties, beyond strict universality, are enjoyed by the second-order translations of existential fixed-point formulas. In particular, do such syntactic properties account for polynomial-time model-checking?
Let alpha is an element of (0, 1)(R) be irrational and G(n) = G(n,1/n alpha) be the random graph with edge probability 1/n(alpha);we know that it satisfies the 0-1 law for first order logic. We deal with the failure o...
详细信息
ISBN:
(纸本)9783319235349;9783319235332
Let alpha is an element of (0, 1)(R) be irrational and G(n) = G(n,1/n alpha) be the random graph with edge probability 1/n(alpha);we know that it satisfies the 0-1 law for first order logic. We deal with the failure of the 0-1 law for stronger logics: L-infinity,L-k, k a large enough natural number and the inductive logic.
We propose an extension of the Ehrenfeucht-Fraisse game able to deal with logics augmented with Lindstrom quantifiers. We describe three different games with varying balance between simplicity and ease of use.
ISBN:
(纸本)9783319235349;9783319235332
We propose an extension of the Ehrenfeucht-Fraisse game able to deal with logics augmented with Lindstrom quantifiers. We describe three different games with varying balance between simplicity and ease of use.
Weighted dense-timed pushdown automata with a timed stack were introduced by Abdulla, Atig and Stenman to model the behavior of real-time recursive systems. Motivated by the decidability of the optimal reachability pr...
详细信息
ISBN:
(纸本)9783319235349;9783319235332
Weighted dense-timed pushdown automata with a timed stack were introduced by Abdulla, Atig and Stenman to model the behavior of real-time recursive systems. Motivated by the decidability of the optimal reachability problem for weighted timed pushdown automata and weighted logic of Droste and Gastin, we introduce a weighted MSO logic on timed words which is expressively equivalent to weighted timed pushdown automata. To show the expressive equivalence result, we prove a decomposition theorem which establishes a connection between weighted timed pushdown languages and visibly pushdown languages of Alur and Mudhusudan;then we apply their result about the logical characterization of visibly pushdown languages.
The question of whether there is a logic that captures polynomial time was formulated by Yuri Gurevich in 1988. It is still wide open and regarded as one of the main open problems in finite model theory and database t...
详细信息
ISBN:
(纸本)9783642150241
The question of whether there is a logic that captures polynomial time was formulated by Yuri Gurevich in 1988. It is still wide open and regarded as one of the main open problems in finite model theory and database theory. Partial results have been obtained for specific classes of structures. In particular, it is known that fixed-point logic with counting captures polynomial time on all classes of graphs with excluded minors. The introductory part of this paper is a short survey of the state-of-the-art in the quest for a logic capturing polynomial time. The main part of the paper is concerned with classes of graphs defined by excluding induced subgraphs. Two of the most fundamental such classes are the class of chordal graphs and the class of line graphs. We prove that capturing polynomial time on either of these classes is as hard as capturing it on the class of all graphs. In particular, this implies that fixed-point logic with counting does not capture polynomial time on these classes. Then we prove that fixed-point logic with counting does capture polynomial time on the class of all graphs that are both chordal and line graphs.
暂无评论