Sciweavers

TCS
2008
14 years 11 days ago
The NP-hardness of finding a directed acyclic graph for regular resolution
Let R be a resolution refutation, given as a sequence of clauses without explicit description of the underlying dag. Then, it is NPcomplete to decide whether R is a regular resolu...
Samuel R. Buss, Jan Hoffmann 0002
LMCS
2006
126views more  LMCS 2006»
14 years 12 days ago
The Completeness of Propositional Resolution: A Simple and Constructive Proof
It is well known that the resolution method (for propositional logic) is complete. However, completeness proofs found in the literature use an argument by contradiction showing tha...
Jean H. Gallier
CADE
1999
Springer
14 years 4 months ago
System Description: CutRes 0.1: Cut Elimination by Resolution
CutRes is a system which takes as input an LK-proof with arbitrary cuts and skolemized end-sequent and gives as output an LKproof with atomic cuts only. The elimination of cuts is ...
Matthias Baaz, Alexander Leitsch, Georg Moser
DNA
2003
Springer
114views Bioinformatics» more  DNA 2003»
14 years 5 months ago
RCA-Based Detection Methods for Resolution Refutation
In molecular resolution refutation, the detection of empty clauses is important. We propose a rolling circle amplification-based detection method for resolution refutation. The ro...
In-Hee Lee, Ji-Yoon Park, Young-Gyu Chai, Byoung-T...