Complexity of resolution proofs and function introduction

DOI10.1016/0168-0072(92)90042-XzbMath0769.03009WikidataQ127087504 ScholiaQ127087504MaRDI QIDQ1194246

Matthias Baaz, Alexander Leitsch

Publication date: 27 September 1992

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

zbMATH Keywords

unsatisfiabilityfunction introduction rulespeed-up over resolution

Mathematics Subject Classification ID

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

Related Items (6)

General form of \(\alpha\)-resolution principle for linguistic truth-valued lattice-valued logic ⋮ Filter-based resolution principle for lattice-valued propositional logic LP\((X)\) ⋮ On the compressibility of finite languages and formal proofs ⋮ Unnamed Item ⋮ Planning with Effectively Propositional Logic ⋮ Cut-elimination and redundancy-elimination by resolution

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The intractability of resolution
• A structure-preserving clause form translation
• Splitting and reduction heuristics in automatic theorem proving
• Theorem proving with variable-constrained resolution
• Hard examples for resolution
• On Different Concepts of Resolution
• Theorem Proving via General Matings
• Lower Bounds on Herbrand's Theorem
• Strong splitting rules in automated theorem proving
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• The Specialization of Programs by Theorem Proving

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