Width and size of regular resolution proofs

Width and size of regular resolution proofs

This paper discusses the topic of the minimum width of a regular resolution refutation of a set of clauses. The main result shows that there are examples having small regular resolution refutations, for which any regular refutation must contain a large clause. This forms a contrast with correspondin...

Full description

Bibliographic Details
Main Author:	Alasdair Urquhart
Format:	Article
Language:	English
Published:	Logical Methods in Computer Science e.V. 2012-06-01
Series:	Logical Methods in Computer Science
Subjects:	computer science - computational complexity mathematics - logic f2.2,f4.1
Online Access:	https://lmcs.episciences.org/862/pdf

Similar Items

Pseudo-finite hard instances for a student-teacher game with a Nisan-Wigderson generator
by: Jan Krajíček
Published: (2012-08-01)

Formalizing Randomized Matching Algorithms
by: Dai Tri Man Le, et al.
Published: (2012-08-01)

Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds
by: Lars Kuhtz, et al.
Published: (2012-10-01)

Absorbing Subalgebras, Cyclic Terms, and the Constraint Satisfaction Problem
by: Libor Barto, et al.
Published: (2012-02-01)

The complexity of global cardinality constraints
by: Andrei A. Bulatov, et al.
Published: (2010-10-01)

Polynomial Size Analysis of First-Order Shapely Functions
by: Olha Shkaravska, et al.
Published: (2009-05-01)

Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
by: Paola Bruscoli, et al.
Published: (2016-05-01)

The complexity of linear-time temporal logic over the class of ordinals
by: Stephane Demri, et al.
Published: (2010-12-01)

Essential Convexity and Complexity of Semi-Algebraic Constraints
by: Manuel Bodirsky, et al.
Published: (2012-10-01)

On the Monadic Second-Order Transduction Hierarchy
by: Achim Blumensath, et al.
Published: (2010-06-01)

Tree-width for first order formulae
by: Isolde Adler, et al.
Published: (2012-03-01)

Verification of Ptime Reducibility for system F Terms: Type Inference in Dual Light Affine Logic
by: Vincent Atassi, et al.
Published: (2007-11-01)

Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix
by: Lê Thành Dũng Nguyên
Published: (2020-02-01)

Guarded Second-Order Logic, Spanning Trees, and Network Flows
by: Achim Blumensath
Published: (2010-02-01)

On the strength of proof-irrelevant type theories
by: Benjamin Werner
Published: (2008-09-01)

From Proof Nets to the Free *-Autonomous Category
by: Francois Lamarche, et al.
Published: (2006-10-01)

Classical BI: Its Semantics and Proof Theory
by: James Brotherston, et al.
Published: (2010-07-01)

The Completeness of Propositional Resolution: A Simple and Constructive Proof
by: Jean Gallier
Published: (2006-11-01)

A proof system for graph (non)-isomorphism verification
by: Milan Banković, et al.
Published: (2023-02-01)

Intuitionistic Layered Graph Logic: Semantics and Proof Theory
by: Simon Docherty, et al.
Published: (2018-10-01)

Perfect Matching in Random Graphs is as Hard as Tseitin
by: Per Austrin, et al.
Published: (2022-12-01)

A Finite-Model-Theoretic View on Propositional Proof Complexity
by: Erich Grädel, et al.
Published: (2022-06-01)

Coherent and finiteness spaces
by: Pierre Hyvernat
Published: (2011-09-01)

Proof-irrelevant model of CC with predicative induction and judgmental equality
by: Gyesik Lee, et al.
Published: (2011-11-01)

A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes
by: Ahmed Bouajjani, et al.
Published: (2009-04-01)

A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems
by: Stéphane Jean Eric Lengrand, et al.
Published: (2011-03-01)

Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
by: Assia Mahboubi, et al.
Published: (2012-02-01)

Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
by: Robert Constable, et al.
Published: (2008-09-01)

A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
by: Andreas Abel, et al.
Published: (2011-05-01)

On linear rewriting systems for Boolean logic and some applications to proof theory
by: Anupam Das, et al.
Published: (2017-04-01)

Some theorems on passing from local to global presence of properties of functions
by: Dimiter Skordev
Published: (2017-04-01)

Completeness for the coalgebraic cover modality
by: Clemens Kupke, et al.
Published: (2012-07-01)

Dynamic Dependency Pairs for Algebraic Functional Systems
by: Cynthia Kop, et al.
Published: (2012-06-01)

Certified Context-Free Parsing: A formalisation of Valiant's Algorithm in Agda
by: Jean-Philippe Bernardy, et al.
Published: (2016-06-01)

$\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
by: Furio Honsell, et al.
Published: (2017-07-01)

Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets
by: Paolo Baldan, et al.
Published: (2008-10-01)

Randomisation and Derandomisation in Descriptive Complexity Theory
by: Kord Eickmeyer, et al.
Published: (2011-09-01)

Modalities in homotopy type theory
by: Egbert Rijke, et al.
Published: (2020-01-01)

Simplified Algorithmic Metatheorems Beyond MSO: Treewidth and Neighborhood Diversity
by: Dušan Knop, et al.
Published: (2019-12-01)

Event Structures for Petri nets with Persistence
by: Paolo Baldan, et al.
Published: (2018-09-01)