@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Name: Oyster Keywords: intuitionistic, propositions as types, refinement, program extraction, Nuprl Description: Edinburgh implementation of the Nuprl System (q.v.) Semantics: intuitionistic type theory, based on Martin Lof type theory Deductive machinery: proof by refinement in natural deduction calculus Dynamics: definitions Persistence: definitions, part-proofs, theorems, lemmas (q.v. CLAM for library facilities) Contact persons: dream@ai.ed.ac.uk User group: ? Pragmatics: ? Documentation: @inproceedings(pub507, key = "Bundy @i", author = "Bundy, A. and van Harmelen, F. and Horn, C. and Smaill, A.", title = "The {Oyster-Clam} system", booktitle = "10th International Conference on Automated Deduction", publisher = "Springer-Verlag", editor = "Stickel, M.E.", pages = "647-648", year = 1990, note = "Lecture Notes in Artificial Intelligence No. 449. Also available from Edinburgh as DAI Research Paper 507.") @Techreport(wp214 , Key = "Horn" , Author = "Horn,C." , Title = "The {Nurprl} Proof Development System" , Institution = DAI , Type = "Working paper" , Number = 214 , Note = "The Edinburgh version of Nurprl has been renamed Oyster." , Year = 1988) Applications: Program synthesis, ? Extensions/enhancements: Resource requirements: Oyster 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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%