QuProlog Home

Qu-Prolog is an extended Prolog designed primarily as a prototyping language and tactic language for interactive theorem provers. It is the implementation language for the Ergo theorem prover.

Qu-Prolog provides support for symbolic computation on notations which appear in mathematics and in specification languages such as Z. Highlights include support for arbitrary quantifiers with parallel bindings and optional typing information, and support for higher-order notations such as function-valued expressions. The unification algorithm is correspondingly extended to support these features.

Qu-Prolog is multi-threaded and provided high-level communication between threads, processes and machines.Together, these features provide a simple, yet powerful mechanism for agent programming.

Distinctive features of Qu-Prolog include:

a separate type of Prolog variable to represent object-level variables;
support for quantified terms;
notations for substitution application;
an implicit parameter mechanism --- a modal logic programming capability whose practical effect is to provide a form of backtrackable assignment;
support for efficient higher-order programming;
support for logic programming of interactive applications by enabling query processing to extend across multiple queries (implemented as variants of read and write that provide access to Prolog variables across multiple input and output events);
management of goal delays;
multiple threads;
high-level symbolic communication between threads, processes and machines in a uniform way;
a heap garbage collector;
a dynamic database garbage collector; and
indexing on the dynamic database.

Qu-Prolog Terms

Assuming all and lambda has been declared as a quantifier (e.g. op(500, quant, all)) and x and y have been declared as object variable prefixes (e.g. obvar_prefix([x,y]) ) then the following are valid Qu-Prolog terms.

all x A - a quantified term whose quantifier is all, whose bound variable is x, and whose body is A .
all x:nats A - same as above but with a term attached to the bound variable - typically used to add types.
all [x:nats, y:nats] A - same as above but with a parallel binding for two object variables.
!!integral(A,B) x f(x) - a quantified term whose quantifer is not a declared atom (the !! is a quantifier escape).
[A/x, B/y]C - a substitution term - all free occurrences of x and y in C are respectively replaced by A and B.
(lambda x A)(B) - a compound term whose functor is a quantified term.
F(A) - a compound term whose functor is a variable.

Delayed Goals

Any goal can be delayed using delay_until/2 and Qu-Prolog can generate both unification delays and not-free-in delays during unification. Users can access the delays with get_delays/1.

Threads

A thread is created with the goal thread_fork(ThreadID, ThreadGoal) that starts executing the goal ThreadGoal in a new thread named ThreadID. Threads are controlled with calls to predicates such as thread_yield, thread_sleep, thread_wait_on_goal and thread_kill.

Communication

Qu-Prolog threads communicate using symbolic addresses that are similar to email addresses. The following are examples of the use of symbolic communication.

Term ->> ThreadID - sends Term to the thread named ThreadID on the same process.
Term ->> ThreadID:ProcessName - same as above but sent to a thread on the named process.
Term ->> ThreadID:ProcessName@MachineAddress - same as above but sent to the given machine.
Term <<- Address - read the next message from the message buffer.
Term <<= Address - search the message buffer for a message that unifies with Term and whose address unifies with Address

There is also a message_choice predicate that provides powerful message buffer searching.

Examples

Example programs that process lambda terms: lambda.ql, lambda2.ql,lambda_type.ql
A simple natural deduction style theorem prover: natural_deduction.ql
A program that attempts to find unifiers for delayed unification problems: incomplete_unify.ql
A Linda tuple server and client - uses multiple-threads and high-level communication: linda_server.ql linda-client.ql
A database that can be queried by client threads (in other processes): db.ql
A simple producer/comsumer example using Elvin communiction: producer.ql , consumer.ql

Manuals

The Qu-Prolog reference manual: postscript refman.ps (560K) and html MAIN.html (central page is 250K)
The Qu-Prolog user manual: userman.ps

Downloads

Qu-Prolog is provided free for any non-comercial use and runs on Unix and Linux machines. The release comes with the above manuals and example programs.

Download Qu-Prolog 6.1: Qu-Prolog 6.1 (1Mbytes)

Release: Qu-Prolog 6.2

New features:

better use of C++ standard classes - now compiles under gcc 3 compilers.
simplified thread scheduler and thread blocking management.
reworking of message classes - by providing a message base class we are now better able to support other communication models (such as Elvin).

Apart from the modified Tcl/Tk interpreter, Qu-Prolog 6.2 will run on MacOSX - see the INSTALL file for details.

Download Qu-Prolog 6.2: Qu-Prolog 6.2 (1Mbytes)

Release: Qu-Prolog 6.3

New features:

Elvin subscription/notification communication added.

Download Qu-Prolog 6.3: Qu-Prolog 6.3 (1Mbytes)

Release: Qu-Prolog 6.4

New features:

Elvin discovery added
increased compatibility with ISO standard
predicates declared as dynamic that appear in a file being compiled are compiled as dymamic predicates rather than producing an error message
some bug fixes

(Thanks to Paulo Moura for suggestions and bug reports.)

Download Qu-Prolog 6.4: Qu-Prolog 6.4 (1Mbytes)

Release: Qu-Prolog 6.5

New features:

QT GUI added - provides GUI support for MacOSX users (and an alternative for Linux users).
Some minor problems with make files fixed

Download Qu-Prolog 6.5: Qu-Prolog 6.5 (1Mbytes)

Release: Qu-Prolog 6.7

New features:

The use of Qu-Prolog terms in Elvin subscriptions added.
Some minor problems fixed

Download Qu-Prolog 6.7: Qu-Prolog 6.7 (1Mbytes)

Release: Qu-Prolog 7.0

New features:

Floating point numbers added (finally!).
Extension to thread_wait_on_goal to allow waits on specific predicates

Download Qu-Prolog 7.0: Qu-Prolog 7.0 (1Mbytes)

Release: Qu-Prolog 7.1

New features:

Bugs for MACOSX users fixed.
Hash table added.

Download Qu-Prolog 7.1: Qu-Prolog 7.1 (1Mbytes)

Release: Qu-Prolog 7.2

New features:

Bugs fixed.
icm_connected and icm_ping added

Download Qu-Prolog 7.2: Qu-Prolog 7.2 (1Mbytes)

Release: Qu-Prolog 7.4

New features:

Strings added.

Download Qu-Prolog 7.4: Qu-Prolog 7.4 (1Mbytes)

Release: Qu-Prolog 8.0

New features:

Elvin and ICM communication has been replaced by Pedro communication.

Download Qu-Prolog 8.0: Qu-Prolog 8.0 (1Mbytes)

Release: Qu-Prolog 8.1

New features:

-g initial-goal option added to the interpreter - initial-goal is executed before the interpreter starts.

Download Qu-Prolog 8.1: Qu-Prolog 8.1 (1Mbytes)

Release: Qu-Prolog 8.2

bug fix in message_choice

Download Qu-Prolog 8.2: Qu-Prolog 8.2 (1Mbytes)

New Release: Qu-Prolog 8.3

bug fix in messages

Download Qu-Prolog 8.3: Qu-Prolog 8.3 (1Mbytes)

For more information about Qu-Prolog, contact the Peter Robinson at: pjr@itee.uq.edu.au.

Feedback on any aspect is also welcome.