检索结果-内蒙古大学图书馆

26th Annual IEEE Symposium on logic in computer science (LICS)

作者： Madelaine, Florent Martin, Barnaby Univ Auvergne Clermont Univ LIMOS BP 10448 F-63000 Clermont Ferrand France Univ Durham Sch Engn & Comp Sci Durham DH1 3LE England

ISBN: (纸本)9780769544120

We classify completely the complexity of evaluating positive equality-free sentences of first-order logic over a fixed, finite structure D. This problem may be seen as a natural generalisation of the quantified constraint satisfaction problem QCSP (D). We obtain a tetrachotomy for arbitrary finite structures: each problem is either in L, is NP-complete, is co-NP-complete or is Pspace-complete. Moreover, its complexity is characterised algebraically in terms of the presence or absence of specific surjective hyper-endomorphisms;and, logically, in terms of relativisation properties with respect to positive equality-free sentences. We prove that the meta-problem, to establish for a specific D into which of the four classes the related problem lies, is NP-hard. Keywords: Galois Connection, Quantified Constraint Satisfaction, Universal Algebra, Computational Complexity, logic in computer science.

关键词： Computational Complexity Galois connection logic in computer science Quantified Constraint Satisfaction Universal Algebra

来源：评论

学校读者我要写书评

暂无评论

Abstract deduction and inferential models for type theory

引用

INFORMATION AND COMPUTATION 2010年第7期208卷 737-771页

作者： Gentilini, Paolo Martelli, Maurizio IMATI CNR I-16149 Genoa Italy Univ Genoa DISI I-16146 Genoa Italy

An inferential semantics for full Higher Order logic (HOL) is proposed. The paper presents a constructive notion of model, that being able to capture relevant computational aspects is particularly suited for the applications of HOL to computer science. The inferential semantics is based on the introduction of new abstract deduction structures (ADS) that express the action of the Comprehension Axiom in a Higher Order logic proof. The ADS's allow to define an inferential algebra of higher order potential proof-trees, endowed with two binary operations, the abstraction and the contraction, each consisting of constructive reductions between potential proofs. Typed formulas are interpreted by sequent trees, and the operations between trees correspond to the logical connectives of the interpreted formula. Higher Order logic is sound and complete w.r.t. the given inferential semantics. (C) 2010 Elsevier Inc. All rights reserved.

关键词： logic in computer science Constructive semantics for Higher Order logic Proof-theory

来源：评论

学校读者我要写书评

暂无评论

EVOLVING MULTIALGEBRAS UNIFY ALL USUAL SEQUENTIAL COMPUTATION MODELS

EVOLVING MULTIALGEBRAS UNIFY ALL USUAL SEQUENTIAL COMPUTATIO...

引用

27th International Symposium on Theoretical Aspects of computer science (STACS)

作者： Grigorieff, Serge Valarcher, Pierre CNRS LIAFA Case 7014 F-75205 Paris 13 France Univ Paris Diderot Paris 7 F-75205 Paris 13 France Univ Paris Est LACL IUT Fontainebleau Senart F-77300 Fontainebleau France

ISBN: (纸本)9783939897163

It is well-known that Abstract State Machines (ASMs) can simulate "step-by-step" any type of machines (Turing machines, RAMs, etc.). We aim to overcome two facts: 1) simulation is not identification, 2) the ASMs simulating machines of some type do not constitute a natural class among all ASMs. We modify Gurevich's notion of ASM to that of EMA ("Evolving MultiAlgebra") by replacing the program (which is a syntactic object) by a semantic object: a functional which has to be very simply definable over the static part of the ASM. We prove that very natural classes of EMAs correspond via "literal identifications" to slight extensions of the usual machine models and also to grammar models. Though we modify these models, we keep their computation approach: only some contingencies are modified. Thus, EMAs appear as the mathematical model unifying all kinds of sequential computation paradigms.

关键词： Abstract state machines Models of machines Computability Universality logic in computer science Theory of algorithms

来源：评论

学校读者我要写书评

暂无评论

IS RAMSEY'S THEOREM ω-AUTOMATIC?

IS RAMSEY'S THEOREM <i>ω</i>-AUTOMATIC?

引用

27th International Symposium on Theoretical Aspects of computer science (STACS)

作者： Kuske, Dietrich CNRS Bordeaux France Lab Bordelais Rech Informat LaBRI Bordeaux France

ISBN: (纸本)9783939897163

We study the existence of infinite cliques in omega-automatic (hyper-) graphs. It turns out that the situation is much nicer than in general uncountable graphs, but not as nice as for automatic graphs. More specifically, we show that every uncountable omega-automatic graph contains an un countable co-context-free clique or anticlique, but not necessarily a context-free (let alone regular) clique or anticlique. We also show that uncountable omega-automatic ternary hyper graphs need not have uncountable cliques or anticliques at all.

关键词： logic in computer science Automata Ramsey theory

来源：评论

学校读者我要写书评

暂无评论

On the Containment of Forbidden Patterns Problems

On the Containment of Forbidden Patterns Problems

引用

16th Annual International Conference on the Principles and Practice of Constraint Programming

作者： Madelaine, Florent IUT Informat LIMOS CNRS UMR 6158 F-63172 Aubiere France

ISBN: (纸本)9783642153952

Forbidden patterns problems are a generalisation of (finite) constraint satisfaction problems which are definable in Feder and Vardi's logic MMSNP [1]. in fact, they are examples of infinite constraint satisfaction problems with nice model theoretic properties introduced by Bodirsky [2]. In previous work [3], we introduced a normal form for these forbidden patterns problems which allowed us to provide an effective characterisation of when a problem is a finite or infinite constraint satisfaction problem. One of the central concepts of this normal form is that of a recolouring. In the presence of a recolouring from a forbidden patterns problem Omega(1) to another forbidden patterns problem Omega(2), containment of Omega(1) in Omega(2) follows. The converse does not hold in general and it remained open whether it did in the case of problems being given in our normal form. In this paper, we prove that this is indeed the case. We also show that the recolouring problem is Pi(p)(2)-harpd and in Sigma(p)(3).

关键词： Constraint Satisfaction Graph Homomorphism logic in computer science Monadic Second Order logic Computational Complexity

来源：评论

学校读者我要写书评

暂无评论

NAMED MODELS IN COALGEBRAIC HYBRID logic

NAMED MODELS IN COALGEBRAIC HYBRID LOGIC

引用

27th International Symposium on Theoretical Aspects of computer science (STACS)

作者： Schroeder, Lutz Pattinson, Dirk DFKI Bremen Bremen Germany Univ Bremen Dept Comp Sci Bremen Germany Imperial Coll London Dept Comp London England

ISBN: (纸本)9783939897163

Hybrid logic extends modal logic with support for reasoning about individual states, designated by so-called nominals. We study hybrid logic in the broad context of coalgebraic semantics, where Kripke frames are replaced with coalgebras for a given functor, thus covering a wide range of reasoning principles including, e.g., probabilistic, graded, default, or coalitional operators. Specifically, we establish generic criteria for a given coalgebraic hybrid logic to admit named canonical models, with ensuing completeness proofs for pure extensions on the one hand, and for an extended hybrid language with local binding on the other. We instantiate our framework with a number of examples. Notably, we prove completeness of graded hybrid logic with local binding.

关键词： logic in computer science semantics deduction modal logic coalgebra

来源：评论

学校读者我要写书评

暂无评论

Isomorphic Implication

引用

THEORY OF COMPUTING SYSTEMS 2009年第1期44卷 117-139页

作者： Bauland, Michael Hemaspaandra, Edith Rochester Inst Technol Dept Comp Sci Rochester NY 14623 USA Leibniz Univ Hannover D-30167 Hannover Germany

We study the isomorphic implication problem for Boolean constraints. We show that this is a natural analog of the subgraph isomorphism problem. We prove that, depending on the set of constraints, this problem is in P, or is NP-complete, or is NP-hard, coNP-hard, and in P (aEuro-) (NP) . We show how to extend the NP-hardness and coNP-hardness to P (aEuro-) (NP) -hardness for some cases, and conjecture that this can be done in all cases.

关键词： Computational complexity Propositional logic Constraints Isomorphism problem logic in computer science

来源：评论

学校读者我要写书评

暂无评论

Functional systems in the context of temporalxmodal logics with indexed flows

引用

INTERNATIONAL JOURNAL OF computer MATHEMATICS 2009年第1-11期86卷 1696-1706页

作者： Burrieza, A. de Guzman, I. P. Munoz-Velasco, E. Univ Malaga Dept Appl Math E-29071 Malaga Spain Univ Malaga Dept Philosophy E-29071 Malaga Spain

We consider logics which define different properties of functions - such as injectivity, surjectivity, monotonicity, etc. - in the context of temporalxmodal logic. In this type of logics, the possible worlds semantics is modified by considering each world as a temporal flow and using accessibility functions to represent the connection among them. This approach is adequate to model interactions between processes with clocks that can be either synchronized or not. We study the definability and give indexed axiomatic systems for these properties.

关键词： temporal logic modal logic logic in computer science definability TxW-logics functional axiomatic systems

来源：评论

学校读者我要写书评

暂无评论

The complexity of equality constraint languages

引用

THEORY OF COMPUTING SYSTEMS 2008年第2期43卷 136-158页

作者： Bodirsky, Manuel Kara, Jan Humboldt Univ Algorithms & Complex Dept Berlin Germany Charles Univ Prague Fac Math & Phys Dept Appl Math Prague Czech Republic

We classify the computational complexity of all constraint satisfaction problems where the constraint language is preserved by all permutations of the domain. A constraint language is preserved by all permutations of the domain if and only if all the relations in the language can be defined by boolean combinations of the equality relation. We call the corresponding constraint languages equality constraint languages. For the classification result we apply the universal-algebraic approach to infinite-valued constraint satisfaction, and show that an equality constraint language is tractable if it admits a constant unary polymorphism or an injective binary polymorphism, and is NP-complete otherwise. We also discuss how to determine algorithmically whether a given constraint language is tractable.

关键词： constraint satisfaction logic in computer science computational complexity clones on infinite domains

来源：评论

学校读者我要写书评

暂无评论

The complexity of equality constraint languages 1

引用

International computer science Symposium in Russia (CSR 2006)

作者： Bodirsky, Manuel Kara, Jan Humboldt Univ Algorithms & Complex Dept Berlin Germany Charles Univ Prague Fac Math & Phys Dept Appl Math Prague Czech Republic

ISBN: (数字)9783540341680

ISBN: (纸本)9783540341666

关键词： constraint satisfaction logic in computer science computational complexity clones on infinite domains

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：