There is no best -normalization strategy for higher-order reasoners

DOI10.1007/978-3-662-48899-7_23MaRDI QIDQ3460064zbMATH OpenOpenAlexFDO

Authors Alexander Steen, Christoph Benzmüller

Publication date 12 January 2016

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-48899-7_23

Mathematics Subject Classification ID

Data structures (68P05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Effective normalization techniques for HOL
• Optimal normalization in orthogonal term rewriting systems
• Higher-order term indexing using substitution trees
• scientific article; zbMATH DE number 6792365
• Term rewriting for normalization by evaluation.

Cited in

(4)

• Making higher-order superposition work
• Effective normalization techniques for HOL
• Making higher-order superposition work
• Extending a high-performance prover to higher-order logic

Describes a project that uses

Uses Software

• Teyjus
• LeoPARD
• QMLTP
• Abella
• Twelf
• TPTP
• Beluga

This page was built for publication: There is no best \(\beta \)-normalization strategy for higher-order reasoners

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