{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,5]],"date-time":"2026-04-05T13:59:36Z","timestamp":1775397576510,"version":"3.50.1"},"reference-count":28,"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\/50008-4","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"335-367","source":"Crossref","is-referenced-by-count":85,"title":["Computing Small Clause Normal Forms"],"prefix":"10.1016","author":[{"given":"Andreas","family":"Nonnengart","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/B978-044450813-3\/50008-4_bb0010","series-title":"The problem was posed at the fourth workshop on automated deduction","article-title":"A challenge problem for automated theorem provers","author":"Andrews","year":"1979"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50008-4_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\/50008-4_bb0020","first-page":"273","article-title":"Normal form transformations","volume":"Vol. I","author":"Baaz","year":"2001"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50008-4_bb0025","doi-asserted-by":"crossref","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\/50008-4_bb0030","first-page":"19","article-title":"Resolution theorem proving","volume":"Vol. I","author":"Bachmair","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0035","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\/50008-4_bb0040","series-title":"Computer Science and Applied Mathematics","article-title":"Symbolic Logic and Mechanical Theorem Proving","author":"Chang","year":"1973"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0045","first-page":"1635","article-title":"Model checking","volume":"Vol. II","author":"Clarke","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0050","series-title":"Relative Complexities of First Order Calculi","author":"Eder","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0055","series-title":"Logic Programming and Automated Reasoning, 5th International Conference, LPAR'94","first-page":"69","article-title":"On the value of antiprenexing","author":"Egly","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50008-4_rf0060","first-page":"10","article-title":"The halting problemml: An automatically generated proof","volume":"30","author":"Egly","year":"1995","journal-title":"AAR Newsletter"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0065","first-page":"1791","article-title":"Resolution decision procedures","volume":"Vol. II","author":"Ferm\u00fcller","year":"2001"},{"issue":"6","key":"10.1016\/B978-044450813-3\/50008-4_bb0070","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":"Logic Journal of the IGPL"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0075","series-title":"Proceedings of the 8th Int. Symp. on Methodologies for Intelligent Systems","article-title":"BDDs and automated deduction","author":"Goubault","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0080","first-page":"30","article-title":"Challenge problem 1","volume":"72","author":"Henschen","year":"1980","journal-title":"SIGART Newsletter"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0085","series-title":"Automated Theorem Proving: A Logical Basis, Vol. 6 of Fundamental Studies in Computer Science","author":"Loveland","year":"1978"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0090","first-page":"371","article-title":"Paramodulation-based theorem proving","volume":"Vol. I","author":"Nieuwenhuis","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0095","article-title":"Strong skolemization","author":"Nonnengart","year":"1996","journal-title":"Research Report MPI-I-96-2-010, Max-Planck-Institut f\u00fcr Informatik, Im Stadtwald, D-66123 Saarbr\u00fccken, Germany"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0100","series-title":"15th International Conference on Automated Deduction, CADE-15","first-page":"397","article-title":"On generating small clause normal forms","author":"Nonnengart","year":"1998"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50008-4_bb0105","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/BF00881919","article-title":"A note on assumptions about skolem functions","volume":"15","author":"Ohlbach","year":"1995","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0110","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\/50008-4_bb0115","series-title":"Transformations of first-order formulae for automated reasoning, Diplomarbeit, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany","author":"Rock","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0120","first-page":"4","article-title":"Logisch-kombinatorische Untersuchungen \u00fcber die Erf\u00fcllbarkeit oder Beweisbarkeit mathematischer S\u00e4tze nebst einem Theoreme \u00fcber dichte Mengen","volume":"4","author":"Skolem","year":"1920","journal-title":"Skrifter utgit av Videnskappsellkapet i Kristiania"},{"key":"10.1016\/B978-044450813-3\/50008-4_rf0125","series-title":"Studies in Constructive Mathematics and Mathematical Logic","article-title":"On the complexity of derivations in propositional calculus","author":"Tseitin","year":"1968"},{"key":"10.1016\/B978-044450813-3\/50008-4_rf0130","series-title":"Automation of Reasoning: Classical Papers on Computational Logic","first-page":"466","article-title":"On the complexity of derivations in propositional calculus","author":"Tseitin","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0130","series-title":"Automation of Reasoning: Classical Papers on Computational Logic","first-page":"466","article-title":"On the complexity of derivations in propositional calculus","author":"Tseitin","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0135","first-page":"1965","article-title":"Combining superposition, sorts and splitting","volume":"Vol. II","author":"Weidenbach","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50008-4_bb0140","series-title":"16th International Conference on Automated Deduction, CADE-16","article-title":"System description: Spass version 1.0.0","author":"Weidenbach","year":"1999"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500084?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500084?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\/B9780444508133500084"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":28,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50008-4","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}