Complexity of resolution proofs and function introduction

DOI10.1016/0168-0072(92)90042-XMaRDI QIDQ1194246zbMATH OpenWikidataFDO

Authors Matthias Baaz, Alexander Leitsch

Publication date 27 September 1992

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0168-0072(92)90042-X

zbMATH Keywords

function introduction rulespeed-up over resolutionunsatisfiability

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Review text

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.

Recommendations

• scientific article; zbMATH DE number 517073
• scientific article; zbMATH DE number 627412
• scientific article; zbMATH DE number 837782
• scientific article; zbMATH DE number 4037813
• Cut rule for the resolution method

Cites work

• A Computing Procedure for Quantification Theory
• A Machine-Oriented Logic Based on the Resolution Principle
• A structure-preserving clause form translation
• Hard examples for resolution
• scientific article; zbMATH DE number 3959369 (Why is no real title available?)
• scientific article; zbMATH DE number 3982555 (Why is no real title available?)
• scientific article; zbMATH DE number 3774914 (Why is no real title available?)
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 3407195 (Why is no real title available?)
• Lower Bounds on Herbrand's Theorem
• On Different Concepts of Resolution
• Splitting and reduction heuristics in automatic theorem proving
• Strong splitting rules in automated theorem proving
• The intractability of resolution
• The Specialization of Programs by Theorem Proving
• Theorem Proving via General Matings
• Theorem proving with variable-constrained resolution

Cited in

(8)

• On the compressibility of finite languages and formal proofs
• General form of \(\alpha\)-resolution principle for linguistic truth-valued lattice-valued logic
• scientific article; zbMATH DE number 517073 (Why is no real title available?)
• Planning with effectively propositional logic
• Certification of prefixed tableau proofs for modal logic
• An Introduction to Lower Bounds on Resolution Proof Systems
• Cut-elimination and redundancy-elimination by resolution
• Filter-based resolution principle for lattice-valued propositional logic LP(X)

This page was built for publication: Complexity of resolution proofs and function introduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1194246)