CMU Artificial Intelligence Repository
FRAPPS: Framework for Resolution-based Automated Proof
FRAPPS (Framework for Resolution-based Automated Proof Procedures) is
a portable resolution theorem-prover written in Common Lisp.
It facilitates the construction of a wide variety of resolution-based
deductive systems. FRAPPS offers the basic functionality necessary to
build such systems, freeing users from low-level implementation
concerns. It is not intended for use in the construction of
high-performance theorem provers, but rather to provide a modular and
customizable system useful for rapid prototyping and experimentation
in teaching and research. An extension to FRAPPS, called "Hooked on
FRAPPS" or "Constraints in FRAPPS" enables the introduction of
specialized unification procedures and constraints.
Version: 2.0 (27-JUN-92)
Requires: Common Lisp
Copying: Copyright (c) 1992 by the Board of Trustees of the
Univ. of Illinois
Use, copying, modification, and distribution permitted
for education, research, and non-profit purposes. For
incorporation into commercial products, please contact
If you are using a copy of FRAPPS, please send a short
note to Prof. Alan M. Frisch .
CD-ROM: Prime Time Freeware for AI, Issue 1-1
Author(s): Alan M. Frisch, Tomas E. Uribe, Michael K. Mitchell
Contact: Prof. Alan M. Frisch
Department of Computer Science
University of Illinois
1304 W. Springfield Avenue
Urbana, IL 61801
Authors!Frisch, Authors!Mitchell, Authors!Uribe,
Automated Reasoning, Clausal Form, Constraints, FOPC, FRAPPS,
Lisp!Code, OTTER, Reasoning!Automated Reasoning,
Resolution Theorem Proving, Theorem Proving,
Univ. of Illinois
and the CADE-11 system description
doc.tgz FRAPPS manual, the "hooked-on-frapps" manual,
formulas into clausal form.
Can be used to translate arbitrary FOPC
convert.tgz OTTER-to-FRAPPS input file translator.
frapps.tgz FRAPPS, including the extension to constraints
Tomas E. Uribe, Alan M. Frisch and Michael K. Mitchell, "An Overview
of FRAPPS 2.0: A Framework for Resolution-based Automated Proof
Procedure Systems", in D. Kapur, editor, Lecture Notes in Computer
Science: 11th International Conference on Automated Deduction,
Springer-Verlag, New York, 1992.
Last Web update on Mon Feb 13 10:27:29 1995