On different structure-preserving translations to normal form

DOI10.1006/jsco.1996.0044zbMath0876.03009OpenAlexW2070717151MaRDI QIDQ674761

Uwe Egly

Publication date: 6 March 1997

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/jsco.1996.0044

zbMATH Keywords

automated deductionHerbrand complexitystructure-preserving normal forms

Mathematics Subject Classification ID

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

Related Items

An answer to an open problem of Urquhart, Non-elementary speed-ups in proof length by different variants of classical analytic calculi, On the practical value of different definitional translations to normal form, A solver for QBFs in negation normal form, Some pitfalls of LK-to-LJ translations and how to avoid them, Practically useful variants of definitional translations to normal form

Uses Software

• OTTER