Effective Normalization Techniques for HOL

DOI10.1007/978-3-319-40229-1_25zbMath1475.68453OpenAlexW2500310339MaRDI QIDQ2817937

Max Wisniewski, Christoph Benzmüller, Kim Kern, Alexander Steen

Publication date: 5 September 2016

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: http://orbilu.uni.lu/handle/10993/40840

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

Extensional higher-order paramodulation in Leo-III ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Agent-Based HOL Reasoning

Uses Software

• LEO-II
• Nitpick
• Isabelle/HOL
• SPASS
• TPTP
• Satallax
• CVC4
• Leo-III
• FLOTTER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The higher-order prover \textsc{Leo}-II
• Isabelle/HOL. A proof assistant for higher-order logic
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Satallax: An Automatic Higher-Order Prover
• Cut-Simulation and Impredicativity
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder

This page was built for publication: Effective Normalization Techniques for HOL