CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

SEQUEL: For generating type-secure and efficient Lisp programs.

SEQUEL (SEQUEnt processing Language) is designed both as a general purpose AI language for generating type-secure and efficient Lisp programs and as a very high level specification language for implementing logics on the computer. Designed at the University of Leeds, SEQUEL compiles sequent-calculus specifications of arbitrary logics to working proof assistants. The sequent calculus specifications are compiled into Horn clauses and from Horn clauses into virtual machine instructions of an abstract machine SLAM (SequeL Abstract Machine) which then translates these instructions into efficient Lisp code using WAM-style compilation techniques. Although a functional programming language, SEQUEL includes facilities for backtracking usually associated with logic programming, and supports a pattern-matching method of building functions based on Prolog notation. The Lisp code generated from SEQUEL functions is completely portable and runs in most Common Lisp implementations. It is comparable in efficiency with hand-written code. SEQUEL also supports optional static type-checking in the manner of SML and similar languages. With type-checking enabled, all inputs and loaded files are type-checked and the resulting Lisp programs are type-secure. The SEQUEL compiler uses the information gleaned from type-checking to add compiler directives within the generated Lisp functions to produce optimized Lisp programs. SEQUEL includes a UNIX-style top level with its own trace package and type-checking debugger. SEQUEL is also of interest to automated reasoning researchers. It provides a very powerful means of generating proof assistants and theorem provers that have a very fast performance using WAM-derived compilation techniques. The theorem provers are automatically verified. It includes a facility for Datalog and an efficient occurs-check Horn-clause-to-Lisp compiler, a mouse driven graphical interface for all proof assistants and theorem provers built under SEQUEL (currently available only under Lucid). Several demonstration theorem provers for different logics, including FOL, Clarke's logic of space, partial evaluation, set theory, and constructive type theory are available.
Origin:  []

Version: 7.0 (1-FEB-94) Ports: SEQUEL runs under Kyoto CL, Lucid CL, and CMU Common Lisp. Copying: Free for non-commercial purposes. CD-ROM: Prime Time Freeware for AI, Issue 1-1 Author(s): Mark Tarver or . University of Leeds Keywords: Authors!Tarver, Automated Reasoning, FOL, Horn Clauses, Lisp!Tools, Partial Evaluation, Proof Assistants, Reasoning!Automated Reasoning, SEQUEL, SML, Theorem Proving, Type Checking, Type-Secure Lisp, Univ. of Leeds, WAM References: LaTeX documentation is included in the distribution.
Last Web update on Mon Feb 13 10:30:52 1995