Computing Tiny Clause Normal Forms

DOI10.1007/978-3-642-38574-2_7MaRDI QIDQ4928432zbMATH OpenOpenAlexFDO

Authors Noran Azmy, Christoph Weidenbach

Publication date 14 June 2013

Published in Automated Deduction – CADE-24 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-38574-2_7

Mathematics Subject Classification ID

Recommendations

• Computing small clause normal forms
• scientific article; zbMATH DE number 1303351
• Optimizing the clausal normal form transformation
• On Normal Form Computations
• Computation of normal forms
• A recursive approach to compute normal forms
• scientific article; zbMATH DE number 17895
• Underspecified computation of normal forms
• Constructing small tree grammars and small circuits for formulas
• Constructing small tree grammars and small circuits for formulas

Cited in

(4)

• An optimality result for clause form translation
• Computing small clause normal forms
• Semi-intelligible Isar proofs from machine-generated proofs
• scientific article; zbMATH DE number 1303351 (Why is no real title available?)

Describes a project that uses

Uses Software

• SPASS
• TPTP

This page was built for publication: Computing Tiny Clause Normal Forms

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