LambdaClam ( λclam, lclam) is a proof planning system that support proof planning over higher-order domains: System description: Proof planning in higher-order logic with λClam. This system description outlines the λClam system for proof planning in higher-order logic. The usefulness and feasibility of applying higher-order proof planning to a number of types of problem is outlined, in particular the synthesis and verification of software and hardware systems. The use of a higher-order metatheory overcomes problems encountered in Clam because of its inability to reason properly about higher-order objects. λClam is written in λProlog.

References in zbMATH (referenced in 19 articles )

Showing results 1 to 19 of 19.
Sorted by year (citations)

  1. Wirth, Claus-Peter: Computer-assisted human-oriented inductive theorem proving by \itdescente infinie -- a manifesto (2012)
  2. Dennis, Louise Abigail; Green, Ian; Smaill, Alan: The use of embeddings to provide a clean separation of term and annotation for higher order rippling (2011)
  3. Dietrich, Dominik; Schulz, Ewaryst: Crystal: Integrating structured queries into a tactic language (2010)
  4. Melis, Erica; Meier, Andreas; Siekmann, Jörg: Proof planning with multiple strategies (2008)
  5. Andrews, Peter B.; Brown, Chad E.: TPS: A hybrid automatic-interactive system for developing proofs (2006)
  6. Carette, Jacques (ed.); Farmer, William M. (ed.): Proceedings of the 12th symposium on the integration of symbolic computation and mechanized reasoning (Calculemus 2005), Newcastle-upon-Tyne, UK, July 18--19, 2005 (2006)
  7. Dennis, Louise A.; Jamnik, Mateja; Pollet, Martin: On the comparison of proof planning systems: $\lambda$ clam, $\Omega$ mega and IsaPlanner (2006)
  8. Dixon, Lucas; Fleuriot, Jacques: A proof-centric approach to mathematical assistants (2006)
  9. Lyaletski, Alexander; Paskevich, Andrey; Verchinine, Konstantin: SAD as a mathematical assistant -- how should we go from here to there? (2006)
  10. Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge: Computer supported mathematics with $\Omega$MEGA (2006)
  11. Zinn, Claus: Supporting the formal verification of mathematical texts (2006)
  12. Cook, A.; Ireland, A.; Michaelson, G.; Scaife, N.: Discovering applications of higher order functions through proof planning (2005)
  13. Siekmann, Jörg; Benzmüller, Christoph: $\Omega$MEGA: Computer supported mathematics (2004)
  14. Castellini, Claudio; Smaill, Alan: Proof planning for feature interactions: A preliminary report (2002)
  15. Zimmer, Jürgen; Dennis, Louise A.: Inductive theorem proving and computer algebra in the MathWeb Software Bus (2002)
  16. Dennis, Louise A.; Smaill, Alan: Ordinal arithmetic: A case study for rippling in a higher order domain (2001)
  17. Kohlhase, Michael; Franke, Andreas: MBase: Representing knowledge and context for the integration of mathematical software systems (2001)
  18. Lacey, David; Richardson, Julian; Smaill, Alan: Logic program synthesis in a higher-order setting (2000)
  19. Bundy, Alan; Richardson, Julian: Proofs about lists using ellipsis (1999)