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

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

1 2 next

  1. Johansson, Moa: Lemma discovery for induction. A survey (2019)
  2. Boy de la Tour, Thierry; Peltier, Nicolas: Analogy in automated deduction: a survey (2014)
  3. Wirth, Claus-Peter: Computer-assisted human-oriented inductive theorem proving by \textitdescenteinfinie -- a manifesto (2012)
  4. Monroy, Raúl; Bundy, Alan; Green, Ian: On process equivalence = equation solving in CCS (2009)
  5. Korukhova, Yulia: An approach to automatic deductive synthesis of functional programs (2007)
  6. Ireland, Andrew; Ellis, Bill J.; Cook, Andrew; Chapman, Roderick; Barnes, Janet: An integrated approach to high integrity software verification (2006)
  7. Ireland, Andrew; Stark, Jamie: Combining proof plans with partial order planning for imperative program synthesis (2006) ioport
  8. Ireland, Andrew; Stark, Jamie: Combining proof plans with partial order planning for imperative program synthesis (2006) ioport
  9. Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge: Computer supported mathematics with (\Omega)MEGA (2006)
  10. Zinn, Claus: Supporting the formal verification of mathematical texts (2006)
  11. Benzmüller, Christoph; Meier, Andreas; Sorge, Volker: Bridging theorem proving and mathematical knowledge retrieval (2005)
  12. Fiedler, Armin: Natural language proof explanation (2005)
  13. Walther, Christoph; Schweitzer, Stephan: Reasoning about incompletely defined programs (2005)
  14. Siekmann, Jörg; Benzmüller, Christoph: (\Omega)MEGA: Computer supported mathematics (2004)
  15. Archer, Myla: TAME: Using PVS strategies for special-purpose theorem proving (2000)
  16. Boulton, Richard J.; Slind, Konrad: Automatic derivation and application of induction schemes for mutually recursive functions (2000)
  17. Dennis, L. A.; Bundy, A.; Green, I.: Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts (2000)
  18. Ireland, Andrew; Stark, Jamie: Proof planning for strategy development (2000)
  19. Jackson, Mike; Lowe, Helen: System description: Interactive proof critics in XBarnacle (2000)
  20. Walther, C.; Kolbe, T.: Proving theorems by reuse (2000)

1 2 next