CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

FRAPPS: Framework for Resolution-based Automated Proof Procedures

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.
Origin: []

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 the author. 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 Keywords: 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 Contains: 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. (a.k.a. "hooked-on-FRAPPS") frapps.tgz FRAPPS, including the extension to constraints References: 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