@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Name: Clam Keywords: proof-planning, rippling, meta-level reasoning, inductive theorem proving, type theory, Oyster (q.v.) Description: Automatic, tactical theorem prover built on top of Oyster (q.v.) Semantics: As Oyster Deductive machinery: As Oyster Dynamics: Wave-rules (rewrite rules) constructed from equational definitions. Meta-level control provided by proof planning mechanism. Persistence: Full library facilities for object-level and meta-level objects. (proofs, definitions, extract terms, wave-rules, induction schemes etc.) Contact persons: dream@ai.ed.ac.uk User group: ? Pragmatics: ? Documentation: @techreport{note475 ,author = "{van Harmelen}, F." ,title = "The {CLAM} proof planner" ,institution = {DAI} ,year = "1989" ,type = "Blue Book Note" ,number = "475" ,note = "Available in the Blue Book in F11 South Bridge"} @inproceedings(pub349, key = "Bundy", author = "Bundy, A.", title = "The Use of Explicit Plans to Guide Inductive Proofs", organization = "Springer-Verlag", booktitle = CADE9, editor = "Lusk, R. and Overbeek, R.", pages = "111-120", note = "Longer version available from Edinburgh as DAI Research Paper No. 349", year = "1988") @article(pub413, key = "Bundy @i", author = "Bundy, A. and {van Harmelen}, F. and Hesketh, J. and Smaill, A.", title = "Experiments with Proof Plans for Induction", journal = JAR, volume = 7, pages = "303-324", year = 1991, note = "Earlier version available from Edinburgh as DAI Research Paper No 413.") Applications: Program synthesis, inductive theorem proving, non-inductive theorem proving Extensions/enhancements: Resource requirements: Clam is written in Sicstus and Quintus Prolog ? Where-to-get-it: Contact dream@ai.ed.ac.uk for details Info source/date: Ian Green 1 Feb 93 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%