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

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 41 articles )

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

1 2 3 next

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

1 2 3 next