The goal of this group is to explore the use of domainspecific knowledge and natural deduction-based reasoning techniques to construct theorem provers that operate in nontrivial mathematical domains. Two new provers, by Larry IIines and Tie-Cheng Wang, are very much like expert systems, since the prover takes its direction by trying to satisfy "higher level" goals, based on knowledge about theorem proving. These are stand-alone provers, not man-machine systems, which are attacking some fairly difficult theorems in mathematics. In addition to this mainline work on mathematical theorem provers, two auxiliary efforts rely heavily on knowledge-based deduction. Michael Starbird is developing a knowledge-based expert system for an area of geometric topology, particularly for three dimensions.
Features of the GLISP programming system that support knowledge-based programming are described. These include compile-time expansion of object-centered programs, interpretation of messages and operations relative to data type, inheritance of properties and behavior from multiple superclasses, type inference and propagation, conditional compilation, symbolic optimization of compiled code, instantiation of generic programs for particular data types, combination of partial algorithms from separate sources, knowledge-based inspection and editing of data, menu-driven interactive programming, and transportability between Lisp dialects and machines. GLISP is fully implemented for the major dialects of Lisp and is available over the ARPANET.
GLISI' is a high-level language that. is compiled into LISP It provides a versatile abst art,-dnt.at.ypc facility with hierarchical inheritance of pl oprl ties and object,-centered programming GLISP programs are shorter and more readable than equivalent LISP programs The object code produced by GLISP is optimized, making it about as cfflcient as handwritten LISP An integrated programming environment is provided, including automatic incremental compilation, interpretive programming features, and an intelligent display-hased inspector/editor for data and data-type descriptions GLISP code is relatively portahlr; the compiler and the data inspcrtor are implemcntcd for most major dialects of LISI' and arc availablr flee or at nominal cost This research was supported in part by NSF grant SED-7912803 in the Joint National Science Foundation - National Institute of Education Program of Research on Cognitive Processes and the Struct,urr of Knowledge in Science and Mathematics, and in part by the Defense Advanced Resealrh Projects Agency rmdel contract MDA-903-80-c-007 Author's present address: Computer Science Department, University of Texas at Austin, Austin, TX: 78712 GLISP contains ordinary LISP as a sublanguage; LISP code can be mixed with GLISP code, so t,hat no capabilities of the underlying LISP syst,cm arc lost. GLISP has also been ex-!,cndcd as a hardware description language for describing VLSI designs. GLISP Statements GLISP provides several kinds of statements that arc t,ranslated into equivalent, code in 1,ISP; each is identified by a key word at, the front of a list containing the code for the stwtemcnt. Many of these statements are similar to t,hose provided by I'ASC!AL: If..then.else While Repeat Case ...Do ..Until These control st,atements provide A compact Given a. set of name/value pa,irs, the A function creates a new tlat,a st,ruct,urc having t,ht: specified values: (A CIRCLE WITH RADIUS Given the earlier ob.jcct dcscript,ion for CIRCLE, this will compile as: (LIST (APPEND '(0 0)) R) The A function works interpretively as well as wit,hin caonlpiled code Context and Type Inference One of t,hc design goals of CLISP is that program code should be independent of the irnpl T le t,at,ic,rls of the structures manipulated by the code to the grcat,cst, dcgrcc possiblc Inclusion of redundanl t,ype declarations in program code would make the code dependent on the actual inplementwtion of structures; instead, GLISI' relies on type inference and its compile-time context, mechanism to tletcrmine the types of object,s.