Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Marked Items 
Alerts
Order History
Saved Items
All
Favorites
    
Book Chapter Printable view
An Upper Bound for Minimal Resolution Refutations

An Upper Bound for Minimal Resolution Refutations

Book SeriesLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN0302-9743 (Print) 1611-3349 (Online)
VolumeVolume 1584/1999
BookComputer Science Logic
DOI10.1007/10703163
Copyright1999
ISBN978-3-540-65922-8
CategoryContributed Papers
DOI10.1007/10703163_12
Pages171-178
Subject CollectionComputer Science
SpringerLink DateWednesday, October 11, 2006
Add to marked items

Contributed Papers

An Upper Bound for Minimal Resolution Refutations

Hans Kleine Büning1 Contact Information

(1)  Department of Mathematics and Computer Science, University of Paderborn, 33095 Paderborn, Germany
Abstract
We consider upper bounds for minimal resolution refutations of propositional formulas in CNF. We show that minimal refutations of minimal unsatisfiable formulas over n variables and n+k clauses consist of at most 2k–1n2 applications of the resolution rule.

Keywords  propositional formulas - length of proofs - minimal unsatisfiability - resolution

Contact Information Hans Kleine Büning
Email: kbcsl@uni-paderborn.de
Fulltext Preview (Small, Large)
Image of the first page of the fulltext
more options
Find


Export this chapter
Export this chapter as RIS | Text
 
Frequently asked questions | General information on journals and books | Send us your feedback | Impressum | Contact
© Springer. Part of Springer Science+Business Media
Privacy, Disclaimer, Terms and Conditions, © Copyright Information
Remote Address: 38.107.191.110 • Server: mpweb06
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)