Automated theory exploration for interactive theorem proving: an introduction to the Hipster system

DOI10.1007/978-3-319-66107-0_1zbMath1483.68484OpenAlexW2758276286MaRDI QIDQ1687709

Moa Johansson

Publication date: 4 January 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-66107-0_1

Mathematics Subject Classification ID

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

Related Items (3)

Theory exploration powered by deductive synthesis ⋮ Into the Infinite - Theory Exploration for Coinduction ⋮ Hipster

Uses Software

• Isabelle
• Theorema
• Isabelle/HOL
• SMT-LIB
• TPTP
• z3
• HOL
• QuickCheck
• CVC4
• TIP

Cites Work

• Unnamed Item
• Unnamed Item
• Conjecture synthesis for inductive theories
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• 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
• TIP: Tons of Inductive Problems
• TIP: Tools for Inductive Provers
• Automating Inductive Proofs Using Theory Exploration
• Quick specifications for the busy programmer
• Hipster: Integrating Theory Exploration in a Proof Assistant

This page was built for publication: Automated theory exploration for interactive theorem proving: an introduction to the Hipster system