Composable Discovery Engines for Interactive Theorem Proving

DOI10.1007/978-3-642-22863-6_28zbMath1342.68302OpenAlexW2139827631MaRDI QIDQ3088022

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)

Related Items

An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time

Uses Software

• Isabelle
• HOL Light

Cites Work

• Unnamed Item
• Isabelle. A generic theorem prover
• Automation for interactive proof: first prototype
• Algebras for combinatorial search
• Idioms are Oblivious, Arrows are Meticulous, Monads are Promiscuous
• Applicative programming with effects