PROLOG-REQUEST@SU-SCORE.ARPA (Chuck Restivo, The Moderator) (11/06/86)
PROLOG Digest Friday, 7 Nov 1986 Volume 4 : Issue 67
Today's Topics:
Implementation - Theorem Prover,
LP Library - Declarative Language Bibliography, Part O
----------------------------------------------------------------------
Date: 4 Nov 86 19:05:00 GMT
From: David Plaisted <ulysses!unc!plaisted@ucbvax.Berkeley>
Subject: Prolog theorem prover
I have recently programmed a theorem prover in C Prolog
that Prolog programmers may find useful. This prover may
be viewed as an extension of Prolog to full first order
logic, that is, non-Horn clauses. Negation is treated as
in first-order logic, not as in negation by failure. The
input syntax is much the same asthe syntax of Prolog.
The prover uses Prolog style depth-first search with a
gradually increasing depth bound (this is therefore
depth-first iterative deepening). Also, solutions to
subgoals are "cached" so that if a subgoal is seen more
than once, work is not repeated. The prover has a
convenient interface to Prolog source code for predicates
whose solutions may be found more efficiently in Prolog
itself than by the theorem prover. This also permits
interaction with the user to obtain the values of variables,
for example. The prover is capable of general term rewriting
to replace subexpressions by equivalent ones. This prover
has been run on a wide variety of problems and generally
obtains simple proofs in 10 or 20 seconds in C Prolog on a
VAX 780. The listing is about 15 pages long. This makes
the prover relatively easy to understand, so it may be
possible to adapt it to various applications by direct
modification of the source code. The prover has been designed
for use with as little user guidance as possible, for users
who know nothing about theorem proving. It is based on a
modification of the theorem proving strategy described
in Plaisted, D., A simplified problem reduction format,
ArtificialIntelligence 18 (1982) 227-261, and has been
distributed to several sites.
The source code contains information about how to use the
prover. This prover is similar to Stickel's Prolog
technology theorem prover, but does not use contrapositives
of clauses as his does. Also, it is much slower than his,
but does not require the axioms to be compiled. Of course,
using a compiled Prolog would speed up my prover by a large
factor. Don Loveland of Duke has recently developed an
extension of Prolog which is intended for "near-Horn"uses
and which may also be of interest to readers of this
newsgroup.
-- David Plaisted
[ I will plan to post the source for the prover and the
example file in forthcoming issues of the Digest -ed ]
------------------------------
Date: Thu 6 Nov 86 11:19:04-PST
From: Chuck Restivo <Restivo@Score.Stanford.EDU>
Subject: Lauren Smith's Bibliography, Part O
OHSU85a Ohsuga S. & Yamauchi H. Multi-Layer Logic - A Predicate Logic
Including Data Structure as Knowledge Representation Language New
Generation Computing, Vol 3, No 4, pp 403-439 1985
ONAI84a Onai R. & Aso M. & Takeuchi A. An Approach to a Parallel
Inference Machine Based on Control-Driven andData-Driven Mechanisms
ICOT Research Center, Technical Report TR-042 January 1984
ONAI85a * Onai R. & Aso M. & Shimizu H. & Masuda K. & Matsumoto A.
Architecture of a Reduction-Based Parallel Inference Machine : PIM-R
New Generation Computing, Vol 3, No 2, pp 197-228 1985
ONAI85b * Onai R. & Shimizu H. & Masuda K. & Matsumoto A. & Aso M.
Architecture and Evalaution of a Reduction-Based Parallel Inference
Machine : PIM-R in WADA86a, pp 1-12 1985
OOPS86a * OOPS ! Newsletter of the Object Oriented Programming
Society Issue 2 Spring 1986
OSH84 ed. O'Shea T. & Eisenstadt M. Artificial Intelligence Tools,
Techniques and Applications Harper & Row, Publishers, New York 1984
OVER75a * Overbeek R.A. An Implementation of Hyper-Resolution Comp.
and Maths. with Appls., Vol 1, pp 201-214 1975
OVER76a * Overbeek R. & McCharen J. & Wos L. Complexity and Related
Enhancements for Automated Theorem-Proving Programs Computers and
Mathematics With Applications, pp 1-16 1976
OZKA85a * Ozkarahan E.A. Evolution and Implementation of the RAP
Database Machine New Generation Computing, Vol 3, No 3, pp 237-271
1985
------------------------------
End of PROLOG Digest
********************