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 24 articles )

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

1 2 next

  1. Wirth, Claus-Peter: Computer-assisted human-oriented inductive theorem proving by \textitdescenteinfinie -- 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. Dennis, Louise A.: Enhancing theorem prover interfaces with program slice information (2007)
  6. Andrews, Peter B.; Brown, Chad E.: TPS: A hybrid automatic-interactive system for developing proofs (2006)
  7. 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)
  8. Dennis, Louise A.; Jamnik, Mateja; Pollet, Martin: On the comparison of proof planning systems: (\lambda)\textscclam, (\Omega)\textscmegaand \textscIsaPlanner (2006)
  9. Dixon, Lucas; Fleuriot, Jacques: A proof-centric approach to mathematical assistants (2006)
  10. Lyaletski, Alexander; Paskevich, Andrey; Verchinine, Konstantin: SAD as a mathematical assistant -- how should we go from here to there? (2006)
  11. Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge: Computer supported mathematics with (\Omega)MEGA (2006)
  12. Zinn, Claus: Supporting the formal verification of mathematical texts (2006)
  13. Cook, A.; Ireland, A.; Michaelson, G.; Scaife, N.: Discovering applications of higher order functions through proof planning (2005)
  14. Meier, Andreas; Melis, Erica: System description: Multi. A multi-strategy proof planner (2005)
  15. Meier, Andreas; Melis, Erica: Failure reasoning in multiple-strategy proof planning (2005)
  16. Siekmann, Jörg; Benzmüller, Christoph: (\Omega)MEGA: Computer supported mathematics (2004)
  17. Castellini, Claudio; Smaill, Alan: Proof planning for feature interactions: A preliminary report (2002)
  18. Zimmer, Jürgen; Dennis, Louise A.: Inductive theorem proving and computer algebra in the MathWeb Software Bus (2002)
  19. Autexier, Serge: A proof-planning framework with explicit abstractions based on indexed formulas (2001)
  20. Dennis, Louise A.; Smaill, Alan: Ordinal arithmetic: A case study for rippling in a higher order domain (2001)

1 2 next