Prolog - [lptp] ERROR: Undefined procedure: prolog

Author

[lptp] ERROR: Undefined procedure: prolog_listing: (:)/2

student

2005-03-10, 3:57 am

I am trying to get Staerks' lptp package working with SWI-Prolog
on my PC but I keep getting the following error message:

ERROR: Undefined procedure: prolog_listing: (:)/2

For example,

?- consult(lptp).
....
LPTP, Version 1.06, July 21, 1999.
Copyright (C) 1999 by Robert F. Staerk
% /usr/local/lptp/src/lptp compiled 0.42 sec, 10,448 bytes

Yes
?- listing(check).

check(A) :-
ERROR: Undefined procedure: prolog_listing: (:)/2

If I am not mistaken, {:}/2 is declared as

lptp.pl: :- op(970,xfy,:). % two Peano dots, right
associative

Would someone please be so kind as to tell me what is going on here,
and what I have to do to make this problem go away?

Thank you.

Jan Wielemaker

2005-03-10, 8:57 am

On 2005-03-10, student <not@a.b.c.dINVALID> wrote:
>
> I am trying to get Staerks' lptp package working with SWI-Prolog
> on my PC but I keep getting the following error message:
>
> ERROR: Undefined procedure: prolog_listing: (:)/2
>
> For example,
>
> ?- consult(lptp).
> ...
> LPTP, Version 1.06, July 21, 1999.
> Copyright (C) 1999 by Robert F. Staerk
> % /usr/local/lptp/src/lptp compiled 0.42 sec, 10,448 bytes
>
> Yes
> ?- listing(check).
>
>
> check(A) :-
> ERROR: Undefined procedure: prolog_listing: (:)/2
>
> If I am not mistaken, {:}/2 is declared as
>
> lptp.pl: :- op(970,xfy,:). % two Peano dots, right
> associative
>
> Would someone please be so kind as to tell me what is going on here,
> and what I have to do to make this problem go away?

After redefining :, loading other sourcefiles may no longer work.
listing/1 is defined in the library and `autoloaded' if you call
listing, but it cannot be compiled correctly as terms holding : are read
differently.

The cleanest way to solve it is to make sure lptp can work with the default
definition of :. Another reasonable solution is to put lptp in a module
(operators are local to the module). You can also restore the original
definition after loading the file.

--- Jan

student

2005-03-11, 4:00 am

Jan Wielemaker wrote:
>
>
> After redefining :, loading other sourcefiles may no longer work.
> listing/1 is defined in the library and `autoloaded' if you call
> listing, but it cannot be compiled correctly as terms holding : are read
> differently.
>
> The cleanest way to solve it is to make sure lptp can work with the
default
> definition of :. Another reasonable solution is to put lptp in a module
> (operators are local to the module). You can also restore the original
> definition after loading the file.
>
> --- Jan

Thank you.

Sorry for the confusion on my part. Once I realized that xemacs
was not emacs and started using emacs, of course, LPTP started
working exactly as advertised.

For those of you who may not know about LPTP
[http://www.inf.ethz.ch/personal/staerk/lptp.html]:

"LPTP is an interactive theorem prover for the formal
verification of Prolog programs. It is a proof refinement system
that allows a user to construct formal proofs interactively. It
is possible to generate proofs deductively from the assumption
forwards to the goal or goal directed from the goal backwards to
the axioms. LPTP has the ability to search for proofs or parts
of proofs automatically. In the simplest case, LPTP just finds
the name of a lemma that already has been proved and is used at
a certain point in a proof. In the best case, LPTP finds
complete proofs. LPTP has been designed for correctness proofs
of pure Prolog programs. Pure Prolog programs may contain
negation, if-then-else and built-in predicates like is/2, </2
and call/n + 1. The programs, however, have to be free of cut
and database predicates like assert/1 and retract/1 which allow
to modify a program during runtime. The kernel of LPTP is
written in exactly the fragment of Prolog that can be treated in
LPTP. This means that LPTP uses no single cut. Moreover, in
principle it is possible to prove properties of LPTP in LPTP
itself." [user.pdf]

--

Sponsored Links