Complexity of resolution proofs and function introduction (Q1194246): Difference between revisions

From MaRDI portal
RedirectionBot (talk | contribs)
Changed an Item
Import240304020342 (talk | contribs)
Set profile property.
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank

Revision as of 02:28, 5 March 2024

scientific article
Language Label Description Also known as
English
Complexity of resolution proofs and function introduction
scientific article

    Statements

    Complexity of resolution proofs and function introduction (English)
    0 references
    0 references
    0 references
    27 September 1992
    0 references
    The function introduction rule derives from the clause \(C=F_ 1\lor F_ 2\) (with free variables \(y_ 1,\dots,y_ k)\) the Skolemised form of the formula \(C'=Q_ 1 y_ 1 Q_ 2 y_ 2\cdots Q_ k y_ k F_ 1\lor Q_ 1' y_ 1 Q_ 2' y_ 2\cdots Q_ k' y_ k\), where \(Q_ i\) are quantifiers, \(\forall'=\exists\), \(\exists'=\forall\). Since \(C\to C'\) is valid, this rule preserves unsatisfiability. Using Statman's sequence of formulas exhibiting non-elementary speed-up over Herbrand expansions, the authors obtain non-elementary speed-up over resolution for one application of the function introduction rule.
    0 references
    function introduction rule
    0 references
    unsatisfiability
    0 references
    speed-up over resolution
    0 references
    0 references

    Identifiers