Lambda-Clam
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.
Keywords for this software
References in zbMATH (referenced in 19 articles )
Showing results 1 to 19 of 19.
Sorted by year (- Wirth, Claus-Peter: Computer-assisted human-oriented inductive theorem proving by \itdescente infinie -- a manifesto (2012)
- 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)
- Dietrich, Dominik; Schulz, Ewaryst: Crystal: Integrating structured queries into a tactic language (2010)
- Melis, Erica; Meier, Andreas; Siekmann, Jörg: Proof planning with multiple strategies (2008)
- Andrews, Peter B.; Brown, Chad E.: TPS: A hybrid automatic-interactive system for developing proofs (2006)
- 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)
- Dennis, Louise A.; Jamnik, Mateja; Pollet, Martin: On the comparison of proof planning systems: $\lambda$ clam, $\Omega$ mega and IsaPlanner (2006)
- Dixon, Lucas; Fleuriot, Jacques: A proof-centric approach to mathematical assistants (2006)
- Lyaletski, Alexander; Paskevich, Andrey; Verchinine, Konstantin: SAD as a mathematical assistant -- how should we go from here to there? (2006)
- Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge: Computer supported mathematics with $\Omega$MEGA (2006)
- Zinn, Claus: Supporting the formal verification of mathematical texts (2006)
- Cook, A.; Ireland, A.; Michaelson, G.; Scaife, N.: Discovering applications of higher order functions through proof planning (2005)
- Siekmann, Jörg; Benzmüller, Christoph: $\Omega$MEGA: Computer supported mathematics (2004)
- Castellini, Claudio; Smaill, Alan: Proof planning for feature interactions: A preliminary report (2002)
- Zimmer, Jürgen; Dennis, Louise A.: Inductive theorem proving and computer algebra in the MathWeb Software Bus (2002)
- Dennis, Louise A.; Smaill, Alan: Ordinal arithmetic: A case study for rippling in a higher order domain (2001)
- Kohlhase, Michael; Franke, Andreas: MBase: Representing knowledge and context for the integration of mathematical software systems (2001)
- Lacey, David; Richardson, Julian; Smaill, Alan: Logic program synthesis in a higher-order setting (2000)
- Bundy, Alan; Richardson, Julian: Proofs about lists using ellipsis (1999)