{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:53Z","timestamp":1761611213901},"reference-count":70,"publisher":"Elsevier","isbn-type":[{"value":"9780444508133","type":"print"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1016\/b978-044450813-3\/50007-2","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"273-333","source":"Crossref","is-referenced-by-count":25,"title":["Normal Form Transformations"],"prefix":"10.1016","author":[{"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[]},{"given":"Uwe","family":"Egly","sequence":"additional","affiliation":[]},{"given":"Alexander","family":"Leitsch","sequence":"additional","affiliation":[]},{"given":"Jean","family":"Goubault-Larrecq","sequence":"additional","affiliation":[]},{"given":"David","family":"Plaisted","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/B978-044450813-3\/50007-2_bb0010","doi-asserted-by":"crossref","first-page":"414","DOI":"10.2307\/2269949","article-title":"Resolution in Type Theory","volume":"36","author":"Andrews","year":"1971","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50007-2_bb0015","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","article-title":"Theorem Proving via General Matings","volume":"28","author":"Andrews","year":"1981","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0020","series-title":"Proceedings of the Fourth Workshop on Theorem Proving with Analytic Tableaux and Related Methods","first-page":"217","article-title":"Non-elementary Speedups between Different Versions of Tableaux","author":"Baaz","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0025","series-title":"Proceedings of the 9th Annual IEEE Symposium on Logics in Computer Science (LICS'94)","first-page":"213","article-title":"A Non-Elementary Speed Up in Proof Length by Structural Clause Form Transformation","author":"Baaz","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0030","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0168-0072(92)90042-X","article-title":"Complexity of Resolution Proofs and Function Introduction","volume":"57","author":"Baaz","year":"1992","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0035","doi-asserted-by":"crossref","first-page":"353","DOI":"10.3233\/FI-1994-2044","article-title":"On Skolemization and Proof Complexity","volume":"20","author":"Baaz","year":"1994","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/B978-044450813-3\/50007-2_rf0040","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/S0168-0072(98)00026-8","article-title":"Cut Normal Forms and Proof Complexity","volume":"97","author":"Baaz","year":"1999","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0045","series-title":"Proceedings of the Kurt G\u00f6del Colloquium","first-page":"108","article-title":"The Even More Liberalized \u03b4-Rule in Free Variable Semantic Tableaux","author":"Beckert","year":"1993"},{"issue":"11","key":"10.1016\/B978-044450813-3\/50007-2_bb0050","first-page":"357","article-title":"Semantic Construction of Intuitionistic Logic","volume":"19","author":"Beth","year":"1956","journal-title":"Kon. Nederl. Akad. Wetensch. Afd. Let. Med., Nieuwe Serie"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0055","series-title":"Deduction: Automated Logic","author":"Bibel","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0060","series-title":"Proceedings of the 10th International Conference on Automated Deduction: Kaiserslautern, 24.\u201327. Juli 1990","first-page":"558","article-title":"Minimizing the Number of Clauses by Renaming","author":"Boy de la Tour","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0065","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1016\/0747-7171(92)90009-S","article-title":"An Optimality Result for Clause Form Translation","volume":"14","author":"Boy de la Tour","year":"1992","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0070","first-page":"7","article-title":"The Halting Problem","author":"Bruschi","year":"1991","journal-title":"AAR Newsletter"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50007-2_bb0075","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1145\/24658.24665","article-title":"The Halting Problem","volume":"18","author":"Burkholder","year":"1987","journal-title":"SIGACT News"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50007-2_bb0080","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","article-title":"The Relative Efficiency of Propositional Proof Systems","volume":"44","author":"Cook","year":"1979","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0085","series-title":"Proceedings of the 5th Annual ACM Symposium on Theory of Computing","first-page":"135","article-title":"On the Lengths of Proofs in the Propositional Calculus","author":"Cook","year":"1974"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0090","first-page":"4","article-title":"A Mechanical Proof of the Halting Problem in Natural Deduction Style","author":"Dafa","year":"1993","journal-title":"AAR Newsletter"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0095","first-page":"1","article-title":"The Formulation of the Halting Problem is Not Suitable for Describing the Halting Problem","author":"Dafa","year":"1994","journal-title":"AAR Newsletter"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0100","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/BF00156916","article-title":"Are Tableaux an Improvement on Truth-Tables? Cut-Free Proofs and Bivalence","volume":"1","author":"D'Agostino","year":"1992","journal-title":"Journal of Logic, Language and Information"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0105","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1093\/logcom\/4.3.285","article-title":"The Taming of the Cut. Classical Refutations with Analytic Cut","volume":"4","author":"D'Agostino","year":"1994","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0110","doi-asserted-by":"crossref","DOI":"10.1090\/mmono\/067","article-title":"Mathematical Intuitionism. Introduction to Proof Theory","author":"Dragalin","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0115","series-title":"AIMSA 84, Artificial Intelligence \u2014 Methodology, Systems, Applications, Varna, Bulgaria","article-title":"An Implementation of a Theorem Prover Based on the Connection Method","author":"Eder","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0120","series-title":"Relative Complexities of First Order Calculi","author":"Eder","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0125","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1006\/jsco.1996.0044","article-title":"On Different Structure-preserving Translations to Normal Form","volume":"22","author":"Egly","year":"1996","journal-title":"Journal of Symbolic Computation"},{"issue":"1,2","key":"10.1016\/B978-044450813-3\/50007-2_bb0130","doi-asserted-by":"crossref","first-page":"165","DOI":"10.3233\/FI-1997-291208","article-title":"On Definitional Translations to Normal Form for Intuitionistic Logic","volume":"29","author":"Egly","year":"1997","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0135","series-title":"CSL'98","first-page":"90","article-title":"Quantifiers and the System KE: Some Surprising Results","author":"Egly","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0140","first-page":"10","article-title":"The Halting Problem: An Automatically Generated Proof","volume":"30","author":"Egly","year":"1995","journal-title":"AAR Newsletter"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0145","series-title":"Proceedings of the Conference on Automated Deduction","first-page":"403","article-title":"On the Practical Value of Different Definitional Translations to Normal Form","author":"Egly","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0150","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1006\/inco.1999.2861","article-title":"On the Practical Value of Different Definitional Translations to Normal Form","volume":"162","author":"Egly","year":"2000","journal-title":"Information and Computation"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0155","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/FI-1999-391204","article-title":"On Intuitionistic Proof Transformations, Their Complexity and Application to Constructive Program Synthesis","volume":"39","author":"Egly","year":"1999","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/B978-044450813-3\/50007-2_rf0160","first-page":"995","article-title":"Temporal and Modal Logic","volume":"Vol. B","author":"Emerson","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0165","series-title":"Kurt G\u00f6del Collected Works","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0170","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","article-title":"Hyperresolution and Automated Model Building","volume":"6","author":"Ferm\u00fcller","year":"1996","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0175","series-title":"Proof Methods for Modal and Intuitionistic Logics","author":"Fitting","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0180","series-title":"First-Order Logic and Automated Theorem Proving","author":"Fitting","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50007-2_rf0185","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen","year":"1935","journal-title":"Mathematische Zeitschrift"},{"key":"10.1016\/B978-044450813-3\/50007-2_rf0190","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/BF01201363","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen","year":"1935","journal-title":"Mathematische Zeitschrift"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0190","series-title":"Ergebnisse eines Mathematischen Kolloquiums","first-page":"39","article-title":"Eine Interpretation des intuitionistischen Aussagenkalk\u00fcls","author":"G\u00f6del","year":"1933"},{"issue":"6","key":"10.1016\/B978-044450813-3\/50007-2_bb0195","doi-asserted-by":"crossref","first-page":"827","DOI":"10.1093\/jigpal\/3.6.827","article-title":"A BDD-Based Simplification and Skolemization Procedure","volume":"3","author":"Goubault","year":"1995","journal-title":"Journal of the IGPL"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50007-2_bb0200","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/BF00881956","article-title":"The Liberalized \u03b4-Rule in Free Variable Semantic Tableaux","volume":"13","author":"H\u00e4hnle","year":"1994","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0205","series-title":"Sitzungsberichte der Preussischen Akademie der Wissenschaften, Physikalisch-mathematische Klasses","first-page":"42","article-title":"Die formalen Regeln der intuitionistischen Logik","author":"Heyting","year":"1930"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0210","series-title":"Sitzungsberichte der Preussischen Akademie der Wissenschaften, Physikalisch-mathematische Klasses","first-page":"57","article-title":"Die formalen Regeln der intuitionistischen Mathematik ii","author":"Heyting","year":"1930"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0215","series-title":"Introduction to Automata Theory, Languages and Computation","author":"Hopcroft","year":"1979"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0220","first-page":"83","article-title":"Semantical Considerations on Modal and Intuitionistic logic","volume":"16","author":"Kripke","year":"1963","journal-title":"Acta Philosophica Fennica"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0225","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-60605-2","article-title":"The Resolution Calculus","author":"Leitsch","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0230","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1017\/S0027763000018055","article-title":"Eine Darstellung der intuitionistischen Logik in der klassischen","volume":"7","author":"Maehara","year":"1954","journal-title":"Nagoya Mathematical Journal"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50007-2_bb0235","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2268135","article-title":"Some Theorems About the Sentential Calculus of Lewis and Heyting","volume":"13","author":"McKinsey","year":"1948","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0240","series-title":"International Conference on Computer Logic","first-page":"198","article-title":"Gentzen-Type Systems and Resolution Rules. Part I: Propositional Logic","author":"Mints","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0245","series-title":"Logic Colloquium 1990","article-title":"Gentzen-Type Systems and Resolution Rules. Part II: Predicate Logic","author":"Mints","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0250","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/BF01051768","article-title":"Resolution Calculus for the First Order Linear Logic","volume":"2","author":"Mints","year":"1993","journal-title":"Journal of Logic, Language and Information"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0255","series-title":"Constraint Programming","first-page":"289","article-title":"Resolution Strategies for the Intuitionistic Logic","author":"Mints","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0260","series-title":"Proceedings of the 15th International Conference on Automated Deduction (CADE-15","first-page":"397","article-title":"On Generating Small Clause Normal Forms","author":"Nonnengart","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0265","first-page":"335","article-title":"Computing small clause normal forms","volume":"Vol. I","author":"Nonnengart","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50007-2_rf0275","first-page":"1403","article-title":"Encoding two-valued nonclassical logics in classical logic","volume":"Vol. II","author":"Ohlbach","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0275","first-page":"137","article-title":"Lower Bounds for Increasing Complexity of Derivations after Cut Elimination","volume":"88","author":"Orevkov","year":"1979","journal-title":"Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im V. A. Steklova AN SSSR"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0280","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","article-title":"A Structure-Preserving Clause Form Translation","volume":"2","author":"Plaisted","year":"1986","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0285","doi-asserted-by":"crossref","first-page":"62","DOI":"10.4064\/fm-40-1-62-95","article-title":"Algebraic Treatment of the Notion of Satisfiability","volume":"40","author":"Rasiowa","year":"1953","journal-title":"Fundamenta Mathematicae"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0290","series-title":"The Mathematics of Metamathematics","author":"Rasiowa","year":"1963"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50007-2_bb0295","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A Machine-Oriented Logic Based on the Resolution Principle","volume":"12","author":"Robinson","year":"1965","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0300","series-title":"Proc. AMS 75","first-page":"104","article-title":"Lower Bounds on Herbrand's Theorem","author":"Statman","year":"1979"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0305","series-title":"The Collected Papers of Gerhard Gentzen","year":"1969"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0310","series-title":"Proof Theory, Vol. 81 Studies in Logic and the Foundations of Mathematics","author":"Takeuti","year":"1975"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0315","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/BF00885763","article-title":"Proof Strategies in Linear Logic","volume":"12","author":"Tammet","year":"1994","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0320","series-title":"Priciples of Intuitionism","author":"Troelstra","year":"1969"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0325","series-title":"Basic Proof Theory, Vol. 43 of Cambridge Tracts in Theoretical Computer Science","author":"Troelstra","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0330","series-title":"Studies in Constructive Mathematics and Mathematical Logic, Part II","first-page":"234","article-title":"On the Complexity of Derivation in Propositional Calculus","volume":"vol. 8","author":"Tseitin","year":"1968"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0335","series-title":"COLOG-88","first-page":"327","article-title":"A Proof-search Method for the First Order Logic","author":"Voronkov","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0340","series-title":"Proceedings of the Conference on Automated Deduction","first-page":"648","article-title":"Theorem Proving in Non-standard Logics Based on the Inverse Method","author":"Voronkov","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50007-2_bb0345","first-page":"1487","article-title":"Connections in nonclassical logics","volume":"Vol. II","author":"Waaler","year":"2001"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50007-2_bb0350","first-page":"399","article-title":"The Resolution Method without Skolemization","volume":"35","author":"Zamov","year":"1987","journal-title":"Soviet Math. Dokl."}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500072?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500072?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,23]],"date-time":"2020-04-23T01:25:44Z","timestamp":1587605144000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500072"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":70,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50007-2","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}