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

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC 2019年第1期20卷 1–46页

作者： Atserias, Albert Ochremiak, Joanna Univ Politecn Cataluna Dept Ciencies Comp Jordi Girona Salgado 31Omega 231 Barcelona 08034 Catalonia Spain Univ Paris Diderot Paris 7 Inst Rech Informat Fondamentale Case 7014 F-75205 Paris 13 France Univ Cambridge Dept Comp Sci & Technol Comp Lab William Gates Bldg15 JJ Thomson Ave Cambridge CB3 0FD England

We analyze how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional, algebraic, and semialgebraic proof systems, the classical constructions of pp-interpretability, homomorphic equivalence, and addition of constants to a core preserve the proof complexity of the CSP. As a result, for those proof systems, the classes of constraint languages for which small unsatisfiability certificates exist can be characterized algebraically. We illustrate our results by a gap theorem saying that a constraint language either has resolution refutations of constant width or does not have bounded-depth Frege refutations of subexponential size. The former holds exactly for the widely studied class of constraint languages of bounded width. This class is also known to coincide with the class of languages with refutations of sublinear degree in Sums of Squares and Polynomial Calculus over the real field, for which we provide alternative proofs. We then ask for the existence of a natural proof system with good behavior with respect to reductions and simultaneously small-size refutations beyond bounded width. We give an example of such a proof system by showing that bounded-degree Lovasz-Schrijver satisfies both requirements. Finally, building on the known lower bounds, we demonstrate the applicability of the method of reducibilities and construct new explicit hard instances of the graph three-coloring problem for all studied proof systems.

关键词： Constraint satisfaction problem proof complexity reductions gap theorems

来源：评论

学校读者我要写书评

暂无评论

proof complexity of the Cut-free Calculus of Structures

引用

JOURNAL OF LOGIC AND COMPUTATION 2009年第2期19卷 323-339页

作者： Jerabek, Emil Acad Sci Inst Math Prague 11567 1 Czech Republic

We investigate the proof complexity of analytic subsystems of the deep inference proof system SKSg (the calculus of structures). Exploiting the fact that the cut rule (i) of SKSg corresponds to the -left rule in the sequent calculus, we establish that the analyticsystem KSgc has essentially the same complexity as the monotone Gentzen calculus MLK. In particular, KSgc quasipolynomially simulates SKSg, and admits polynomial-size proofs of some variants of the pigeonhole principle.

关键词： proof complexity calculus of structures monotone sequent calculus cut rule

来源：评论

学校读者我要写书评

暂无评论

proof complexity of Modal Resolution

引用

JOURNAL OF AUTOMATED REASONING 2022年第1期66卷 1-41页

作者： Sigley, Sarah Beyersdorff, Olaf Univ Leeds Sch Comp Leeds W Yorkshire England Friedrich Schiller Univ Jena Inst Comp Sci Jena Germany

We investigate the proof complexity of modal resolution systems developed by Nalon and Dixon (J Algorithms 62(3-4):117-134, 2007) and Nalon et al. (in: Automated reasoning with analytic Tableaux and related methods-24th international conference, (TABLEAUX'15), pp 185-200, 2015), which form the basis of modal theorem proving (Nalon et al., in: Proceedings of the twenty-sixth international joint conference on artificial intelligence (IJCAI'17), pp 4919-4923, 2017). We complement these calculi by a new tighter variant and show that proofs can be efficiently translated between all these variants, meaning that the calculi are equivalent from a proof complexity perspective. We then develop the first lower bound technique for modal resolution using Prover-Delayer games, which can be used to establish "genuine" modal lower bounds for size of dag-like modal resolution proofs. We illustrate the technique by devising a new modal pigeonhole principle, which we demonstrate to require exponential-size proofs in modal resolution. Finally, we compare modal resolution to the modal Frege systems of Hrubes (Ann Pure Appl Log 157(2-3):194-205, 2009) and obtain a "genuinely" modal separation.

关键词： Modal logic Resolution proof complexity Lower bounds Prover-Delayer games Pigeonhole principle

来源：评论

学校读者我要写书评

暂无评论

proof complexity and Textual Cohesion

引用

JOURNAL OF LOGIC LANGUAGE AND INFORMATION 2015年第1期24卷 53-64页

作者： Dresner, Eli Tel Aviv Univ Dept Philosophy IL-69978 Ramat Aviv Israel

In the first section of this paper I define a set of measures for proof complexity, which combine measures in terms of length and space. In the second section these measures are generalized to the broader category of ... 详细信息

关键词： proof complexity Text complexity Cohesion Texture

来源：评论

学校读者我要写书评

暂无评论

proof complexity of propositional default logic

引用

ARCHIVE FOR MATHEMATICAL LOGIC 2011年第7-8期50卷 727-742页

作者： Beyersdorff, Olaf Meier, Arne Mueller, Sebastian Thomas, Michael Vollmer, Heribert Leibniz Univ Hannover Inst Theoret Comp Sci Hannover Germany Charles Univ Prague Fac Math & Phys Prague Czech Republic

Default logic is one of the most popular and successful formalisms for non-monotonic reasoning. In 2002, Bonatti and Olivetti introduced several sequent calculi for credulous and skeptical reasoning in propositional default logic. In this paper we examine these calculi from a proof-complexity perspective. In particular, we show that the calculus for credulous reasoning obeys almost the same bounds on the proof size as Gentzen's system LK. Hence proving lower bounds for credulous reasoning will be as hard as proving lower bounds for LK. On the other hand, we show an exponential lower bound to the proof size in Bonatti and Olivetti's enhanced calculus for skeptical default reasoning.

关键词： Default logic Sequent calculus proof complexity

来源：评论

学校读者我要写书评

暂无评论

proof complexity of intuitionistic implicational formulas

引用

ANNALS OF PURE AND APPLIED LOGIC 2017年第1期168卷 150-190页

作者： Jerabek, Emil Czech Acad Sci Inst Math Zitna 25 Prague 11567 1 Czech Republic

We study implicational formulas in the context of proof complexity of intuitionistic propositional logic (IPC). On the one hand, we give an efficient transformation of tautologies to implicational tautologies that preserves the lengths of intuitionistic extended Frege (EF) or substitution Frege (SF) proofs up to a polynomial. On the other hand, EF proofs in the implicational fragment of IPC polynomially simulate full intuitionistic logic for implicational tautologies. The results also apply to other fragments of other superintuitionistic logics under certain conditions. In particular, the exponential lower bounds on the length of intuitionistic EF proofs by Hrubes (2007), generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Jefabek (2009), can be realized by implicational tautologies. (C) 2016 Elsevier B.V. All rights reserved.

关键词： proof complexity Intuitionistic logic Implicational fragment

来源：评论

学校读者我要写书评

暂无评论

proof complexity Lower Bounds from Algebraic Circuit complexity 31

Proof Complexity Lower Bounds from Algebraic Circuit Complex...

引用

31st Conference on Computational complexity (CCC)

作者： Forbes, Michael A. Shpilka, Amir Tzameret, Iddo Wigderson, Avi Princeton Univ Dept Comp Sci Princeton NJ 08544 USA Tel Aviv Univ Dept Comp Sci Tel Aviv Israel Royal Holloway Univ London Dept Comp Sci Egham Surrey England Inst Adv Study Sch Math Princeton NJ 08540 USA

ISBN: (纸本)9783959770088

We give upper and lower bounds on the power of subsystems of the Ideal proof System (IPS), the algebraic proof system recently proposed by Grochow and Pitassi [26], where the circuits comprising the proof come from various restricted algebraic circuit classes. This mimics an established research direction in the boolean setting for subsystems of Extended Frege proofs whose lines are circuits from restricted boolean circuit classes. Essentially all of the subsystems considered in this paper can simulate the well-studied Nullstellensatz proof system, and prior to this work there were no known lower bounds when measuring proof size by the algebraic complexity of the polynomials (except with respect to degree, or to sparsity). Our main contributions are two general methods of converting certain algebraic lower bounds into proof complexity ones. Both require stronger arithmetic lower bounds than common, which should hold not for a specific polynomial but for a whole family defined by it. These may be likened to some of the methods by which Boolean circuit lower bounds are turned into related proof-complexity ones, especially the "feasible interpolation" technique. We establish algebraic lower bounds of these forms for several explicit polynomials, against a variety of classes, and infer the relevant proof complexity bounds. These yield separations between IPS subsystems, which we complement by simulations to create a partial structure theory for IPS systems. Our first method is a functional lower bound, a notion of Grigoriev and Razborov [25], which is a function f : {0,1}n F such that any polynomial f agreeing with f on the boolean cube requires large algebraic circuit complexity. We develop functional lower bounds for a variety of circuit classes (sparse polynomials, depth-3 powering formulas, read-once algebraic branching programs and multilinear formulas) where [f(g) equals l/p(,) for a constant -degree polynomial p depending on the relevant circuit class. We believe

关键词： proof complexity Algebraic complexity Nullstellensatz Subset-Sum

来源：评论

学校读者我要写书评

暂无评论

proof complexity of Modal Resolution Systems

Proof Complexity of Modal Resolution Systems

引用

作者： Sigley, Sarah Elizabeth The University of Leeds

学位级别：博士

In this thesis we initiate the study of the proof complexity of modal resolution systems. To our knowledge there is no previous work on the proof complexity of such systems. This is in sharp contrast to the situation for propositional logic where resolution is the most studied proof system, in part due to its close links with satisfiability solving. We focus primarily on the proof complexity of two recently proposed modal resolution systems of Nalon, Hustadt and Dixon, one of which forms the basis of an existing modal theorem prover. We begin by showing that not only are these two proof systems equivalent in terms of their proof complexity, they are also equivalent to a number of natural refinements. We further compare the proof complexity of these systems with an older, more complicated modal resolution system of Enjalbert and Farinas del Cerro, showing that this older system p-simulates the more streamlined calculi. We then investigate lower bound techniques for modal resolution. Here we see that whilst some propositional lower bound techniques (i.e. feasible interpolation) can be lifted to the modal setting with only minor modifications, other propositional techniques (i.e. size-width) fail completely. We further develop a new lower bound technique for modal resolution using Prover-Delayer games. This technique can be used to establish "genuine" modal lower bounds (i.e lower bounds on the number of modal inferences) for the size of tree-like modal resolution proofs. We apply this technique to a new family of modal formulas, called the modal pigeonhole principle to demonstrate that these formulas require exponential size modal resolution proofs. Finally we compare the proof complexity of tree-like modal resolution systems with that of modal Frege systems, using our modal pigeonhole principle to obtain a "genuinely" modal separation between them.

关键词： modal logic resolution proof complexity

来源：评论

学校读者我要写书评

暂无评论

On the proof complexity of Paris-Harrington and Off-Diagonal Ramsey Tautologies

引用

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC 2016年第4期17卷 1–25页

作者： Carlucci, Lorenzo Galesi, Nicola Lauria, Massimo Univ Rome I Rome Italy Univ Politecn Cataluna C Jordi Girona 1-3Omega 223 ES-08034 Barcelona Catalonia Spain Univ Roma La Sapienza Dipartimento Informat Via Salaria 113 I-00198 Rome Italy

We study the proof complexity of Paris-Harrington's Large Ramsey Theorem for bi-colorings of graphs and of off-diagonal Ramsey's Theorem. For Paris-Harrington, we prove a non-trivial conditional lower bound in Resolution and a non-trivial upper bound in bounded-depth Frege. The lower bound is conditional on a (very reasonable) hardness assumption for a weak (quasi-polynomial) Pigeonhole principle in RES(2). We show that under such an assumption, there is no refutation of the Paris-Harrington formulas of size quasi polynomial in the number of propositional variables. The proof technique for the lower bound extends the idea of using a combinatorial principle to blow up a counterexample for another combinatorial principle beyond the threshold of inconsistency. A strong link with the proof complexity of an unbalanced off-diagonal Ramsey principle is established. This is obtained by adapting some constructions due to Erdos and Mills. We prove a non-trivial Resolution lower bound for a family of such off-diagonal Ramsey principles.

关键词： proof complexity resolution Ramsey's theorem Paris-Harrington's principle

来源：评论

学校读者我要写书评

暂无评论

proof complexity of Resolution-based QBF Calculi 32

Proof Complexity of Resolution-based QBF Calculi

引用

32nd International Symposium on Theoretical Aspects of Computer Science (STACS)

作者： Beyersdorff, Olaf Chew, Leroy Janota, Mikolas Univ Leeds Sch Comp Leeds W Yorkshire England INESC ID Lisbon Portugal

ISBN: (纸本)9783939897781

proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of important QBF solvers. However, the proof complexity of these proof systems is currently not well understood and in particular lower bound techniques are missing. In this paper we exhibit a new and elegant proof technique for showing lower bounds in QBF proof systems based on strategy extraction. This technique provides a direct transfer of circuit lower bounds to lengths of proofs lower bounds. We use our method to show the hardness of a natural class of parity formulas for Q-resolution and universal Q-resolution. Variants of the formulas are hard for even stronger systems as long-distance Q-resolution and extensions. With a completely different lower bound argument we show the hardness of the prominent formulas of Kleine Buning et al. [34] for the strong expansion-based calculus IR-calc. Our lower bounds imply new exponential separations between two different types of resolution-based QBF calculi: proof systems for CDCL-based solvers (Q-resolution, long-distance Q-resolution) and proof systems for expansion-based solvers (for all Exp+Res and its generalizations IR-calc and IRM-calc). The relations between proof systems from the two different classes were not known before.

关键词： proof complexity QBF lower bound techniques separations

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：