The UMA Forum Linear Logic Programming Language



UMA Forum is a logic programming language based on linear logic. Actually, it is an implementation of a subset of Dale Miller's Forum Specification Language developed at the University of Málaga (UMA). UMA Forum is part of a research project concerning linear logic, logic programming, object orientedness and concurrency. Being a research programming language, most of UMA Forum features are subject to change; although it intends to be an efficient implementation of a large portion of Forum.

Currently, the main differences between UMA Forum and Forum are:

  1. untyped term algebra is used as term language instead of simply typed lambda calculus
  2. the universal quantifier is not supported

This means that UMA Forum is not as well-suited as Forum to support abstractions and higher-order programming; but it could support these features in a future. In spite of this, UMA Forum retains a large amount of expressiveness from linear logic.

The main contribution of UMA Forum is a new stack-based resource management system based on the Lolli resource management system, previously developed by Iliano Cervesato, Frank Pfenning and Joshua S. Hodas. The key idea of the new resource management system is that linear logic sequent contexts (i.e. logic programs and goals) can be manipulated as stacks, just as in hereditary Harrop formula based languages like lambda Prolog. In particular, the UMA Forum resource management system represents sequent contexts as stacks instead of multisets, replacing costly union and intersection multiset operations by simple, inexpensive push and pop stack operations. Similarly to the single data structure used in the Lolli implementation, clause order (an important topic in a logic programming language execution model) is preserved by using a single stack to store both linear and classical clauses. This new stack-based approach to resource management simplifies the implementation, providing an efficient linear logic proof search strategy at a very low cost. In addition, the single formula identifier used in the Lolli system is no longer needed. As the original Lolli resource management system, the new UMA Forum system can be easily applied to the implementation of linear logic theorem provers and programming languages, either single or multiple-conclusion. On the other hand, the current UMA Forum resource management system is not complete in the sense it manages additive truth (i.e. top) through backtracking. It will be extended to manage top soon.


UMA Forum is written in (fairly standard) Prolog, so all you need is a Prolog implementation. I have used SICStus Prolog 3 #5 (commercial) under Unix and BinProlog 5.75 (free, by Paul Tarau) under Windows 95/NT and Unix.

It should also be possible to use another Prolog implementation with little or no change.

*** Note to BinProlog 5.75 users:

I have experienced some problems with BinProlog dynamic predicates. In particular, the interpreter switches do not switch well. For example, the user command eager switches to the eager proof search; but sometimes it does not. To solve this, simply repeat the switching user command until the switch is accomplished. This problem does not occur under SICStus Prolog 3 #5.

Download & Installation

The current release of UMA Forum is version 0.1. The files comprising the UMA Forum version 0.1 distribution are contained in the compressed archive umaforum01.tar.gz. To install UMA Forum version 0.1 simply copy this file onto any directory and then ungizp and untar it as follows:

$ ungzip umaforum01.tar.gz
$ tar -xvf umaforum01.tar

Executing UMA Forum

Executing UMA Forum under SICStus Prolog

  1. invoke SICStus Prolog as usual; e.g.

    $ sicstus

  2. reconsult the file

    ?- [forumsu].

  3. enter the query

    ?- forum.

Executing UMA Forum under BinProlog

  1. invoke BinProlog as usual; e.g.

    $ bp

  2. reconsult the file under Unix, or the file under Windows 95/NT

    ?- [forumbu].

  3. enter the query

    ?- forum.

Compiling UMA Forum under SICStus Prolog

Alternatively, you can compile the files to obtain better performance. For example, under SICStus Prolog:

  1. compile the files and

    ?- fcompile([sicstus_unix,forum]).

  2. load the resulting object files

    ?- load([sicstus_unix,forum]).

  3. enter the query

    ?- forum.

In any case, after entering the goal forum you will see the banner and prompt below:

UMA Forum 0.1
author: Pablo Lopez
Dept. of Computer Science
University of Malaga, SPAIN

'help' command available

reading module 'sync' from file 'sync'


Now you can enter user commands to execute and goals to solve.

The UMA Forum Language

UMA Forum is a small but expressive programming language based on a few basic concepts; namely modules, operator declarations, clauses and predefined predicates. Most of its lexical elements are borrowed from Prolog, including variable and functor names, allowed symbols and comments. The anonymous variable _ is also supported (and encouraged through singleton variable warnings). Formal syntax of UMA Forum is available as a BNF-style grammar.


UMA Forum code is organized into modules. A module is a container of operator declarations and clauses. Be aware that real modular programming is not supported yet. UMA Forum modules are mainly intended to distinguish loaded from used clauses. A loaded module is just a module which has been (re)consulted and stored in memory. A used module is a loaded module whose clauses will be used along the proof search of a goal.

As an example, consider a file lists containing the two modules shown below (a source file can contain more than one module):

module one.

infix (::) : 400.

append(X::Xs,Y,X::Z) <= append(Xs,Y,Z).

module two.

length(_::Xs,N1) <= length(Xs,N) <= N1 is N+1.

Now, load both modules by reconsulting the file lists:

Forum> [lists].

and try to solve the goal

Forum> append(X,Y,a::b::c::nil).

UMA Forum will respond

no solution

since modules one and two are loaded, but not used. Now, use module one as follows:

Forum> use(one).

Since the clauses defining predicate append are visible, the previous goal can be solved

Forum> append(X,Y,a::b::c::nil).
X = nil
Y = a::b::c::nil
X = a::nil
Y = b::c::nil
X = a::b::nil
Y = c::nil
X = a::b::c::nil
Y = nil
4 solutions.
no more solutions.

Contrary to most logic programming languages, successive solutions are obtained typing intro, while typing ';' halts proof search. On the other hand, module two remains loaded, but it is not used, so a goal like

Forum> append(X,Y,a::b::c::nil) x length(X,Lx) x Lx<3.

cannot be solved. To solve it, both modules must be used

Forum> use(two).

Hence, by using certain loaded modules you decide the actual logic program used to solve a given goal. This simple mechanism is particularly useful in the presence of linear clauses.

Operator Declarations

UMA Forum supports user defined operators. Operator declarations include position (prefix, infix and postfix), associativity (left, right and non-associative) and precedence level (1..1200, being 1 the highest and 1200 the lowest). As an example, consider the operator declarations below:

 prefix  pre  : 700.   % prefix operator declaration
 infixl  il   : 750.   % infix left associative operator declaration
 infixr  ir   : 750.   % infix right associative operator declaration
 infix   i    : 750.   % infix non associative operator declaration
 postfix post : 800.   % postfix operator declaration

Predefined Operators

In addition to user defined operators and connectives, UMA Forum has the following predefined operators:

            \     :     ,     =     \=     ==     \==     =..
            <     =<    >     >=    +      -      *       /
            mod   is    .     []

The precedence level of the predefined operators and its semantics are inherited from the underlying Prolog system (except for '\' and ':', standing for abstraction and operator declaration respectively). Predefined operators and connectives cannot be redeclared.


UMA Forum clauses are freely generated from the linear logic asynchronous connectives. The ASCII rendering of these connectives is shown in the table below.

Linear LogicASCII
additive truetop
multiplicative falsebot
multiplicative disjunction#
additive conjunction&
linear implication-* , *-
intuitionistic implication=> , <=
why not exponential?
universal quantifierforall

On the other hand, the level of precedence of these connectives from higher to lower is:

ConnectivePrecedence Level
top, bot1
-*, =>650
*-, <=750

UMA Forum clauses are implicitly universally quantified and must be followed by a full stop. Examples of syntactically valid UMA Forum clauses are:

 p(s(X)) # q(s(s(Y))) *- p(X) & q(s(X)) <= q(Y).
 goal(G) # s(on)*- s(off) -* G.
 go <= forall X \ forall Y \ p(x) => q(y).

Note that the universal quantifier forall and the abstraction '\' are not supported yet; but they are reserved.

Linear logic synchronous connectives are supported through second-order predicates as well. Refer to the UMA Forum module sync.

Predefined Predicates

UMA Forum has the following predefined predicates:


Except for printf/1 and printf/2, predefined predicates are taken from the underlying Prolog implementation, so their documentation is available in any Prolog manual or textbook. The predicate printf/2 is modelled after the C printf() standard output function, and works as follows:


The format string contains plain characters, escape sequences and format specifiers. Plain characters are written to the current output stream "as is". Escape sequences are formed by a backslash '\' followed by one of the plain characters below:

characterwritten as
\nnew line

Format specifiers are formed by a percentage symbol '%' followed by a plain character. The ith format specifier affects the way the ith term of the list of terms is written in the current output stream as follows:

format specifierwritten as
%wbuilt in predicate write/1
%dbuilt in predicate display/1
%qbuilt in predicate writeq/1
%sbuilt in predicate put/1 (term must be a list of characters)

The printf/1 predicate is similar to printf/2, but it has no list of terms attached, and hence its format contains no format specifier.

User Commands

Following the prompt Forum> you can enter either a user command to be executed or a goal to be solved. Any UMA Forum term not being a user command is considered to be a goal.

User commands are classified into three categories: configuration commands, module commands and miscellaneous commands. These are described below.

Configuration Commands

lazy sets lazy proof search; i.e. the stack-based resource management system is applied, avoiding backtracking through context splits
eager sets eager proof search; i.e. the resource management system is not active but the interpreter backtracks through all possible context splits.
showtime shows execution time of every solution founded.
hidetime execution time is not shown.
trace displays the sequent before applying the next inference rule.
notrace switchs off tracing.
setedit(name) sets name as default editor command.
switches lists current switches.
reset resets the UMA Forum interpreter to its initial state. First default settings are taken, then the configuration file forum.ini is read to complete the initial configuration of the interpreter, overriding any default setting.

Module Commands

[file,...] reconsults the source files [file,...], loading the contained modules.
modules lists the currently loaded modules.
use(name) the clauses contained in module mame will be used to solve any goal. This way, you can set the logic program currently used.
unuse(name) the clauses contained in module name will not be used to solve a goal. This way, you can set the logic program currently used.
uses lists currently used modules; i.e. the current logic program.
delete(name) deletes module name from memory.
list(name) lists contents of module name.
listing lists contents of all modules.
edit(name) edits the source file containing module name. The actual editing command involved depends on the value of setedit.
edit edits most recently reconsulted source file.

Miscellaneous Commands

dir lists current directory contents.
system(cmd) invokes system command cmd.
halt halts the UMA Forum interpreter, returning control to the Prolog environment.
help shows a help screen.


Both eager and lazy proof search strategies are supported in order to compare the performance of the new resource management method. The examples below are solved in a few milliseconds by the lazy proof search, while they take minutes or even hours to complete when using the eager proof search, clearly showing the appropriateness of the method.


The source code of these and other examples is contained in the distribution archive.

Please, send any comment, correction or suggestion.
Last modified January 12, 1998 by Pablo López (