CLAM
CLAM Proof Planner. OYSTER is an interactive proof editor closely based on the Cornell NuPRL system, but implemented in Prolog. CLAM is a meta-level system built on top of OYSTER to turn the interactive proof editor into a fully automatic theorem proving system.
Keywords for this software
References in zbMATH (referenced in 41 articles )
Showing results 1 to 20 of 41.
Sorted by year (- Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael: TacticToe: learning to prove with tactics (2021)
- Hamami, Yacin; Morris, Rebecca Lea: Plans and planning in mathematical proofs (2021)
- Johansson, Moa: Lemma discovery for induction. A survey (2019)
- Boy de la Tour, Thierry; Peltier, Nicolas: Analogy in automated deduction: a survey (2014)
- Wirth, Claus-Peter: Computer-assisted human-oriented inductive theorem proving by \textitdescenteinfinie -- a manifesto (2012)
- Monroy, Raúl; Bundy, Alan; Green, Ian: On process equivalence = equation solving in CCS (2009)
- Korukhova, Yulia: An approach to automatic deductive synthesis of functional programs (2007)
- Ireland, Andrew; Ellis, Bill J.; Cook, Andrew; Chapman, Roderick; Barnes, Janet: An integrated approach to high integrity software verification (2006)
- Ireland, Andrew; Stark, Jamie: Combining proof plans with partial order planning for imperative program synthesis (2006) ioport
- Ireland, Andrew; Stark, Jamie: Combining proof plans with partial order planning for imperative program synthesis (2006) ioport
- 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)
- Benzmüller, Christoph; Meier, Andreas; Sorge, Volker: Bridging theorem proving and mathematical knowledge retrieval (2005)
- Fiedler, Armin: Natural language proof explanation (2005)
- Walther, Christoph; Schweitzer, Stephan: Reasoning about incompletely defined programs (2005)
- Siekmann, Jörg; Benzmüller, Christoph: (\Omega)MEGA: Computer supported mathematics (2004)
- Archer, Myla: TAME: Using PVS strategies for special-purpose theorem proving (2000)
- Boulton, Richard J.; Slind, Konrad: Automatic derivation and application of induction schemes for mutually recursive functions (2000)
- Dennis, L. A.; Bundy, A.; Green, I.: Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts (2000)
- Ireland, Andrew; Stark, Jamie: Proof planning for strategy development (2000)