CMU Artificial Intelligence Repository
SEQUEL: For generating type-secure and efficient Lisp
programs.
lang/lisp/code/tools/sequel/
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:
agora.leeds.ac.uk:scs/logic/ [129.11.144.130]
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
AI.Repository@cs.cmu.edu