Composable discovery engines for interactive theorem proving

DOI10.1007/978-3-642-22863-6_28MaRDI QIDQ3088022zbMATH OpenOpenAlexFDO

Authors Phil Scott, Jacques D. Fleuriot

Publication date 17 August 2011

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-22863-6_28

Mathematics Subject Classification ID

Computer graphics; computational geometry (digital and algorithmic aspects) (68U05)

Recommendations

• A combinator language for theorem discovery
• An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time
• scientific article; zbMATH DE number 1552511
• Lemma discovery for induction. A survey
• Automated theory exploration for interactive theorem proving: an introduction to the Hipster system

Cites work

• Algebras for combinatorial search
• Applicative programming with effects
• Automation for interactive proof: first prototype
• scientific article; zbMATH DE number 1863397 (Why is no real title available?)
• Idioms are oblivious, arrows are meticulous, monads are promiscuous
• Isabelle. A generic theorem prover

Cited in

(2)

• A combinator language for theorem discovery
• An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time

Describes a project that uses

Uses Software

• Isabelle
• HOL Light

This page was built for publication: Composable discovery engines for interactive theorem proving

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