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.
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.
Pedro also provides peer-to-peer messages and so
Qu-Prolog threads can communicate using symbolic addresses that are similar
to email addresses. The following are examples of the use of symbolic
- 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
- 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 Pedro communiction: producer.ql , consumer.ql
- The Qu-Prolog reference manual: main.pdf (560K) and html MAIN.html (central page is 250K)
- The Qu-Prolog user manual: userman.ps
New Release: Qu-Prolog 9.1 Date:23/08/11
- Slight modification to better support Pedro 1.9 for communications.
Release: Qu-Prolog 9.0 Date:14/07/11
- Qu-Prolog ported to Windows (at last!)
- Bug fixes + minor improvements
Release: Qu-Prolog 8.12 Date:24/11/10
- Added timers - see create_timer in manual.
- Added gettimeofday - get time as a float.
- Added absolute_file_name - file expansion.
- Compiler can now cope with spaces in filename.
- Command line editing/history/completion added (using rlwrap).
- Bug fixes + minor improvements
Download Qu-Prolog 8.12: Qu-Prolog 8.12 (1Mbytes)
Release: Qu-Prolog 8.11 Date:18/06/10
NOTE:Qu-Prolog 8.11 requires Pedro 1.5 or greater for communications because of the change of connection protocol.
- Added two different timers to thread_wait_on_goal. One will cause the call to fail after a given timeout if it hasn't already succeeded. The other rechecks the goal at least as often as the specified timeout.
- Changed protocol for Pedro connections in order to better determine machine names in a variety of network setups.
- improving ISO compatibility
- bug fixes
Download Qu-Prolog 8.11: Qu-Prolog
Release: Qu-Prolog 8.10 Date:01/12/09
- Port to 64bit
- setup_call_cleanup added
- bug fixes
Download Qu-Prolog 8.10: Qu-Prolog
Release: Qu-Prolog 8.9
- Minor improvements in efficiency
- CHR (Constraint Handling Rules) added
Download Qu-Prolog 8.9: Qu-Prolog 8.9 (1Mbytes)
Release: Qu-Prolog 8.8
- Improved efficiency for object trail
- ip_array_get_entries added
Download Qu-Prolog 8.8: Qu-Prolog 8.8 (1Mbytes)
Release: Qu-Prolog 8.7
- Fix compiler bug
Download Qu-Prolog 8.7: Qu-Prolog 8.7 (1Mbytes)
Release: Qu-Prolog 8.6
- Fix make clean
- Fix string escape bug
Download Qu-Prolog 8.6: Qu-Prolog 8.6 (1Mbytes)
Release: Qu-Prolog 8.5
- Uses new pedro connection protocol - needs at least pedro-0.8
- More efficient lookup of IP address and machine name.
Download Qu-Prolog 8.5: Qu-Prolog 8.5 (1Mbytes)
Release: Qu-Prolog 8.3
- bug fix in messages
Download Qu-Prolog 8.3: Qu-Prolog 8.3 (1Mbytes)
Release: Qu-Prolog 8.2
- bug fix in message_choice
Download Qu-Prolog 8.2: Qu-Prolog 8.2 (1Mbytes)
Release: Qu-Prolog 8.1
- -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.0
- Elvin and ICM communication has been replaced by Pedro communication.
Download Qu-Prolog 8.0: Qu-Prolog 8.0 (1Mbytes)
Release: Qu-Prolog 7.4
- Strings added.
Download Qu-Prolog 7.4: Qu-Prolog 7.4 (1Mbytes)
Release: Qu-Prolog 7.2
- Bugs fixed.
- icm_connected and icm_ping added
Download Qu-Prolog 7.2: Qu-Prolog 7.2 (1Mbytes)
Release: Qu-Prolog 7.1
- Bugs for MACOSX users fixed.
- Hash table added.
Download Qu-Prolog 7.1: Qu-Prolog 7.1 (1Mbytes)
Release: Qu-Prolog 7.0
- 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 6.7
- 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 6.5
- 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.4
- 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
Download Qu-Prolog 6.4: Qu-Prolog 6.4 (1Mbytes)
Release: Qu-Prolog 6.3
- Elvin subscription/notification communication added.
Release: Qu-Prolog 6.2
- 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).
Download Qu-Prolog 6.2: Qu-Prolog 6.2 (1Mbytes)
For more information about Qu-Prolog, contact the Peter Robinson at: email@example.com.
Feedback on any aspect is also welcome.