previous   next   up   top

Prolog and Logic Programming



Pure, declarative, and constructive arithmetic all-mode relations

[The Abstract of the paper]
We present decidable logic programs for addition, multiplication, division with remainder, exponentiation, and logarithm with remainder over the unbounded domain of natural numbers. Our predicates represent relations without mode restrictions or annotations. They are fully decidable under the common, DFS-like, SLD resolution strategy of Prolog or under an interleaving refinement of DFS. We prove that the evaluation of our arithmetic goals always terminates, given arguments that share no logic variables. Further, the (possibly infinite) set of solutions for a goal denotes exactly the corresponding mathematical relation. (For SLD without interleaving, and for some infinite solution sets, only half of the relation's domain may be covered.) We define predicates to handle unary (for illustration) and binary representations of natural numbers, and prove termination and completeness of these predicates. Our predicates are written in pure Prolog, without cut ! , var/1 , or other non-logical operators. The purity and minimalism of our approach allows us to declare arithmetic in other logic systems, such as Haskell type classes.

To prove decidability, correctness and other properties of our predicates we have developed a new semantics of normal logic programs: solution sets. Unlike dominant model-theoretic semantics, ours is operational, proof-theoretic. It is more abstract than the partial-trace semantics.

We emphasize two premises of the paper. First, writing all-mode arithmetic relations is, in general, straightforward: with var/1 we determine which of the arguments of, say, the add predicate are instantiated, and so use addition, subtraction, or numeral generation as appropriate. We may chose to propagate the addition constraint or to residualize. There is a good reason however why the use of var/1 is discouraged. In our paper, we specifically disavowed var/1 , negation or other such (reflective) facilities. We deliberately limited ourselves to Horn clauses, and nothing else. Theorem provers and constraint solvers certainly offer very sophisticated procedures for solving arithmetic constraints. In any such procedures, to my knowledge, we must know where all our variables are. But in our paper, we specifically do not. We have no idea which arguments of our goals are or contain variables, and we cannot tell. We disclaim any and all intensional analysis, just so we could see how much we can do without.

Our use of SLD resolution and its simple variants -- as widely implemented and quite efficient -- was another self-imposed restriction. One may quite rightfully say that we deliberately painted ourselves into the corner. On the other hand, purity and minimalism, however difficult to live with, often offer deep and general insights.

In contrast to Presburger arithmetic, which can decide arbitrary formulas within its domain, we can fully decide only base predicates -- addition, multiplication, etc. -- but not their conjunctions, or conjunctions with equality. Conjunctions of the base predicates let us express arbitrary Diofantine equations, which are not generally decidable. Technically, after a base goal succeeds, its arguments may share logic variables. Many of our termination theorems will not therefore apply to the second goal in a conjunction. It appears that some (if not many or all) cases of divergence due to the sharing of logic variables in the arguments of a goal could be prevented by tabling. Investigating the evaluation strategy of the XSB system is future work. Also part of the future work is the evaluation of principled ways of introducing negation, e.g., as done in lambda-Prolog.

The goal of this project was not to be useful but to be insightful. Quite surprisingly to us, a similar development for Curry proved to be practically useful and has become part of a Haskell Curry implementation.

Joint work with William E. Byrd, Daniel P. Friedman, and Chung-chieh Shan.

The current version is January 2008.
arithm.pdf [209K]
Pure, Declarative, and Constructive Arithmetic Relations (Declarative Pearl)
The paper presented at FLOPS 2008, 9th International Symposium on Functional and Logic Programming. Ise, Japan, April 14-16, 2008. The paper is published in Springer's Lecture Notes in Computer Science 4989/2008, pp. 64-80. < >

Chung-chieh Shan. Slides of the talk at FLOPS08, April 14, 2008.
< >

unary.prl [9K]
Warm-up: a stepwise development of addition and multiplication of unary numbers

pure-bin-arithm.prl [41K]
Extensively commented source code, with termination proofs

DefinitionTree.hs [14K]
Definitional trees, a model for reasoning about evaluation of normal logic programs
That file is a full-fledged Prolog interpreter in Haskell. The salient feature is the absence of name-generation effects. The evaluation strategy is no longer concerned with fresh name generation, and so is easier to reason about.


Universal quantification, impredicative terms, and effects

This note discusses universal quantification of variables in the body of a clause, given open- and closed-world assumptions. We also discuss two ways of expressing impredicative terms like (exists U. [U,U]) , and `common subexpression elimination' in logical programs. We draw parallels with effects, of creating logical variables.
The current version is 1.3, March 5, 2005.
quantification.txt [9K]


Soutei, a logic-based trust-management system

[The Abstract of the paper]
We describe the design and implementation of a trust-management system Soutei, a dialect of Binder, for access control in distributed systems. Soutei policies and credentials are written in a declarative logic-based security language and thus constitute distributed logic programs. Soutei policies are modular, concise, and readable. They support policy verification, and, despite the simplicity of the language, express role- and attribute-based access control lists, and conditional delegation.

We describe the real-world deployment of Soutei into a publish-subscribe web service with distributed and compartmentalized administration, emphasizing the often overlooked aspect of authorizing the creation of resources and the corresponding policies.

Soutei brings Binder from a research prototype into the real world. Supporting large, truly distributed policies required non-trivial changes to Binder, in particular mode-restriction and goal-directed top-down evaluation. To improve the robustness of our evaluator, we describe a fair and terminating backtracking algorithm.

This is a joint work with Andrew Pimlott.

The current version is April 2006.
Soutei.pdf [405K]
Soutei, a logic-based trust-management system (system description)
The paper presented at FLOPS 2006, 8th International Symposium on Functional and Logic Programming. Fuji-Susono, Japan, April 24-26, 2006. The paper is published in Springer's Lecture Notes in Computer Science 3945/2006, pp. 130-145. < >

soutei-1.tar.gz [61K]
The first implementation of Soutei, in Scheme. Its compiles Soutei assertions into Kanren code. The code relies on Bigloo-specific module system and the built-in parser and lexer. The code can be compiled with Bigloo v2.4. It includes many built-in tests.
This source code is given here for information only. It is no longer used; it served as a model for the current, version 2 implementation, which is written in Haskell.

< >
Version 2.1 of Soutei: the Haskell library and several sample applications


Beyond pure Prolog: power and danger

First-order Horn-clause logic is often called pure Prolog. Negation-as-failure, copy_term/2 , cut, and var/1 are `impure', extra-logical features. Each of them makes a logic program more expressive, and potentially illogical. Every occurrence of an impure feature must be justified lest our program computes nonsense. We summarize here compelling applications of impure features and embarrassingly trivial ways to write unsound programs. A programmer must balance the extra power of impure features against the extra trouble of ensuring their safe use.

Cut, !/0 , is common in logic programs. Lee Naish has argued that without cut or a similar committed choice operator one cannot write any large practical logic program. It has been rigorously proven that without negation and pruning, many simple Datalog queries cannot be answered in polynomial time and space. Cut or negation are especially useful for writing deterministic computations with ML-like pattern-matching. Adding an element to a list unless the list already contains the element is very difficult to write in pure Prolog: the naive program

     	insert(X,L,L) :- member(X,L).
derives not only the goal insert(1,[1,2],[1,2]) but also the undesired goal insert(1,[1,2],[1,1,2]) with the duplicate element in the result list.

The power of impure features comes at a significant cost: it becomes difficult to see what the program computes and if it makes sense. The simple minimal-model or fix-point semantics no longer apply. If impure features are used improperly, the logic program may give wrong results. There is no `less impure' feature in our list: negation, copy_term/2 , and cut alone can express var/1; the latter is trivially unsound. We illustrate the danger on trivial examples, often one-liners. The danger is well-known but bears repetition. To avoid confusing the emulated var/1 with the built-in predicate of the same name, we shall use the name vr/1 .

Danger of var/1

The goal var(Term) succeeds if Term is a free variable. The variable remains unbound. The predicate var/1 is indispensable for implementing relations such as sum(X,Y,Z) (relating arbitrarily instantiated arguments by X+Y=Z) relying on the efficient native arithmetic of Prolog.

Alas var/1 also lets us easily write programs that give wrong results.

     vr(X) :- var(X).
     foo(X) :- vr(X), X=1.
For uniformity, we use the name vr/1 and define it here as the alias to the built-in var/1 . We first ask the question if there is a value of X that makes foo(X) derivable from the current database of rules and facts. The Prolog system says yes and gives one such value, 1:
     ?- foo(X).
     X = 1
     ?- foo(1).

If we verify the answer and check if indeed foo(1) is derivable from the current knowledge, we get the answer no. With var/1 , logic programming becomes programming in inconsistent logic. We cannot generally trust any results.

Danger of negation-as-failure

Prolog's built-in negation predicate \+/1 is just as dangerous as var/1: indeed, negation can express var/1 in one line:

     vr(X) :- \+ \+ (X=0), \+ \+ (X=1).
Only a variable can be, alternatively, unified with two distinct atoms (e.g., 0 and 1). The double-negation is symptomatic. The evaluation of ?-vr(X). succeeds with the answer X=_G180 (the variable X remains unbound). Goals vr(0) , vr(1) , vr(2) , vr([0]) , and vr([X|Y]) all fail.

In the above example, the cause of unsoundness is obvious: the negated goal \+ (X=0) binds an existing free variable. This is called ``floundering''. Some Prolog systems report a run-time warning or an error in this case (floundering is not decidable statically). SWI Prolog, which is used for all tests here, lets floundering go undetected.

Danger of copy_term/2

The well-known elegant implementation of lambda-calculus in Prolog relies on copy_term/2 . Because of that, copy_term/2 is the least objected to. Alas, copy_term/2 , too, expresses var/1 , also in one line:

     vr(X) :- copy_term(X,0), copy_term(X,1).
Danger of cut

Finally, cut, by itself expresses var/1:

     noteq(X,X) :- !, fail.
     vr(X) :- (noteq(X,0), !, fail); (noteq(X,1), !, fail); true.
Lee Naish: Pruning in logic programming
An advanced tutorial at the International Conference on Logic Programming, 13-16 June, 1995, Japan.
< >
Lee Naish makes a rarely mentioned point that without pruning (done by negation, cut, or committed choice operators) large logical programs become impractical because they run our of space. Pruning removes choice-points and lets GC collect stack frames and variables. Section 4 of the paper describes the condition upon which soft-cut, negation, and even once are sound. Essentially, this is the groundness condition: the evaluation of a negated or pruned goal must not instantiate any free variable that existed before the evaluation. Alas, it is not decidable to statically assure that condition.

Fosca Giannotti, Dino Pedreschi, Carlo Zaniolo: Declarative Semantics of Pruning Operators in Logic Programming
Methods of Logic in Computer Science, v1 (1994), pp. 61-76.
< >
Section 1 gives a lucid introduction to choice operators.

Fosca Giannotti, Dino Pedreschi, Carlo Zaniolo: Semantics and Expressive Power of Nondeterministic Constructs in Deductive Databases
Journal of Computer and System Sciences, V62, N1 (2001), pp. 15-42.
< >
The paper proves that non-deterministic choice operators are essential in expressing PTIME queries.

Alberto Momigliano: Elimination of Negation in a Logical Framework
Ph.D. Thesis. CMU-CS-00-175, December 15, 2000.
< >
``In spite of its limits, it can be shown that Horn logic has the same computational power of every other programming language [Apt90]. Moreover, Horn logic has some nice model-theoretic properties, namely the minimum model property; it is natural to consider the latter as the declarative meaning or the intended interpretation of a program. Therefore it has been argued that we should be content with Horn logic, which seems to be a complete and reasonably efficient computational logic. However, many have been dissatisfied with the difficulty to express even the easiest logical problems in a language that lacks (explicit) disjunction and negation.''


Lambda-calculator and alpha-conversion in pure Prolog

Implementing lambda-calculus in Prolog well illustrates the power and inconvenience of pure Prolog, and similarity and differences between logic variables and variables of lambda-calculus. At first sight, the two kinds of variables appear the same: a variable is a placeholder for a term, a named hole. An occurrence of a variable in a term marks the spot where some other term can be inserted into at some later time. Once the hole marked by a variable is filled in, the variable is gone and no further substitution at that place is possible. The above description characterizes both logic variables and variables of lambda-calculus, leading to the elegant implementation of call-by-value or call-by-name lambda-calculus in Prolog. We write E1 * E2 for an application and X->E for an abstraction, `binding' the variable X in the body E . X is supposed to be a free logic variable. Here is the first attempt at eval(E,R) , which relates the expression E with its result R .
     eval(E1*E2, R)   :- eval(E1, (X->Body)), eval(E2,E2R), X=E2R, eval(Body,R).

The relation eval(E,R) implements call-by-value evaluation, reducing the argument E2 of the application before substituting it into the body of the abstraction. The act of substitution is performed when we unify X , the `lambda-bound' variable, with the value of the argument: X=E2R . The effect is as if at that moment all occurrences of X in the Body of the abstraction are replaced with E2R . Since we use logic variables for variables of lambda-calculus, Prolog's built-in substitution machinery does lambda-calculus substitutions: normalization by evaluation.

Although our eval/2 works in many simple cases -- e.g., eval((F->F*1)*(X->X), R) unifies R with 1 -- our code is flawed. Evaluating eval((X->X) * (X->X), R) gives a wrong result. A Prolog system with the sound unification cannot substitute X->X for X in the body of the first abstraction: the unification in X=X->X fails the occurs check. Many Prolog systems omit the occurs check, and so succeed at the substitution. Alas, the result is the term X->X where X is no longer a free logic variable. We can no longer apply X->X by unifying X with an arbitrary term. A Prolog term X->Body where X is not a free variable does not represent a lambda-abstraction. It does not help if the user took care to use distinct logic variables for different bound variables. This property is not preserved in the course of the evaluation, when applying non-linear lambda-abstractions, with several occurrences of the bound variable in its body. For example, the first application in (F->F*(F * 1))*(X->X) gives us (X->X)*(X->1) with two different bound variables represented by the same logic variable. The further evaluation is derailed. We need to uniquely rename all bound variables before each substitution: we need the explicit alpha-conversion!

Prolog does have a built-in predicate to copy a term replacing all existing free logic variables with fresh ones: copy_term/2 . The correct evaluation relation is:

     eval(E1*E2, R) :- eval(E1, E1R), eval(E2,E2R), copy_term(E1R,(E2R->Body)),

Now, eval((F->F*(F * 1))*(X->X),R) and even eval((F-> (F * F) * (F * 1)) * (X -> X), R) succeed unifying R with 1. Furthermore,

     Mul   = (C1->C2->F-> C1 * (C2 * F)),
     Two   = (F->X-> F * (F * X)),
     Succ  = (N->F->X-> N * F * (F * X)),
     Three = (Succ * Two),
     eval(Mul * Two * Three * s * z,R).
succeeds with R = s* (s* (s* (s* (s* (s*z))))) .

However, copy_term/2 is impure and quickly leads to unsoundness. Can we prove that the use of copy_term/2 in the lambda-calculator is sound? Better yet, can we implement the evaluation relation in pure Prolog, in Horn-clause logic? Yes, we can indeed emulate copy_term/2 to the extent needed for the alpha-conversion. The idea is to traverse a term, instantiating free variables with ground terms of the form v(unique_counter) , maintaining the invariant that distinct variables are replaced with distinct terms. When we come across X->Body we attempt to instantiate X with a ground term v(unique_counter) . Chances are X is not a free variable, having been already bound in the course of traversal. The desired invariant holds nevertheless. We associate v(counter) with a fresh logic variable Xnew in the traversal environment, and traverse the Body , replacing v(counter) with the associated Xnew . At the end of the traversal we obtain BodyNew and reconstruct the abstraction Xnew->BodyNew . We are now sure that Xnew is free and unique. The pure Prolog code below implements this idea: the goal alpha_convert(E,R) alpha-converts the input lambda-term E and unifies the result with R . The real work is done by alpha_convert(Cin,Cout,Env,E,ER) where Cin and Cout are the counters for building terms of the form v(unique_counter) , and Env is the traversal environment associating v(counter) with Xnew . If our lambda calculus includes constants, we require them to be of the form c(constant_term) . In addition, we assume that the original term E is closed, so we could start the traversal in the empty environment. This restriction is easy to lift. We use unary numerals [] , [u] , [u,u] , etc. for the unique counter.

     unlt([],[u|_]). unlt([u|T1],[u|T2]) :- unlt(T1,T2).
     uneq(U1,U2) :- unlt(U1,U2); unlt(U2,U1).
     alpha_convert(E,R) :- alpha_convert([],_,[],E,R).
     alpha_convert(Cin,Cout,Env,E1*E2,E1R*E2R) :-
       alpha_convert(Cin,C,Env,E1,E1R), alpha_convert(C,Cout,Env,E2,E2R).
     alpha_convert(Cin,Cout,Env,X->Body,Xnew->BodyNew) :-
       C=[u|Cin], X = v(C1), (C1 = Cin; unlt(C1,C)),
     alpha_convert(Cin,Cin,[(v(C1),_)|T],v(C),R) :-
       uneq(C1,C), alpha_convert(Cin,Cin,T,v(C),R).
Here unlt(U1,U2) is the less-than relation on unary numbers, and uneq/2 is the unary number disequality. The evaluation of alpha_convert((X -> (X->X) * (X->X) * X), R) unifies R with _G275-> (_G295->_G295)* (_G309->_G309)*_G275 , as desired. We can write the lambda-calculator in pure Prolog thusly:
     eval(E1*E2, R) :- alpha_convert(E1*E2,E1C*E2C),
                       eval(E1C,X->Body), eval(E2C,E2R), X=E2R, eval(Body,R).
As before, the goal eval((F->F*(F * c(1)))*(X->X),R) succeeds and unifies R with c(1) . The multiplication example works too; we should remember to wrap all constants in c(...) .


Exceptions in logic programming

We describe two different modes of exception handling in logic programming: cutting choice points upon raising an exception, and preserving choice points. The former behavior is prescribed by the ISO Prolog. We argue for the alternative, which yields generators. The preservation of choice points also makes exception handling cheaper. We present the implementation of choice-point--preserving exceptions in Kanren and Hansei.

Logic programs by nature have a form of exceptions: fail. Failure of a goal in a conjunction terminates further evaluation of the conjunction. A disjunction plays the role of exception handling, catching the failure and invoking the second disjunct to `handle' it.

Failure as a form of exceptions is not sufficient. Unlike success (which is accompanied by the current substitution, with the bindings for logic variables), failure carries no information and has no flavors. Success comes in many forms; failure is singular. Often an informative failure and nuanced failure handling is desired. One example is parsing, which was the first and still is the compelling application of logic programming. The laconic NO as the parsing result is infuriatingly unhelpful, especially for large input. The error ought to be described and pin-pointed. Furthermore, some failures of parsing are provisional, indicating the need to try another parsing alternative. Some other parsing errors (e.g., of lexing) should be treated as definite and immediately reported to the user. As another example, an undefined predicate ought to be treated differently from other failures, and handled not by initiating backtracking but by trying to locate the missing predicate (e.g., search for a predicate with a similar spelling; attempt to load an external library; etc). For these reasons, Prolog systems from early on had an ad hoc exception handling. ISO Prolog codified these practices, as catch/3 and throw/1 predicates. Here is their specification (quoted from the SWI Prolog documentation):

catch(:Goal, +Catcher, :Recover)
``Behaves as call/1 if no exception is raised when executing Goal. If an exception is raised using throw/1 while Goal executes, and the Goal is the innermost goal for which Catcher unifies with the argument of throw/1, all choice-points generated by Goal are cut, the system backtracks to the start of catch/3 while preserving the thrown exception term and Recover is called as in call/1. The overhead of calling a goal through catch/3 is very comparable to call/1. Recovery from an exception is much slower, especially if the exception-term is large due to the copying thereof.''
``Raise an exception. The system looks for the innermost catch/3 ancestor for which Exception unifies with the Catcher argument of the catch/3 call. ISO demands throw/1| to make a copy of Exception, walk up the stack to a catch/3 call, backtrack and try to unify the copy of Exception with Catcher.''

We stress the discarding of choice points after an exception is raised. In the following example, the exception cuts the choice X=4:

     ?- catch((X=1;X=2;throw(3);X=4),Z,true).
     X = 1 ;
     X = 2 ;
     Z = 3.

Kanren implements the catch/3 and throw/1 predicates with the ISO Prolog interface. However, choice points are not discarded when the exception is raised. Therefore, the exception term does not have to be copied, and exception recovery is cheap. Here is the illustration.

     (run #f (q)
       (fresh (y)
           (fresh (x)
              (succeed (== x 1))
              (succeed (== x 2))
              (succeed (== x 3) (throw `(e1 5)))
              (succeed (== x 4) (throw `(e1 15)))
              (succeed (== x 5)))
            (== q `(no-exc ,x)))
          `(e1 ,y)
          (== q `(caught 1 ,y)))))
The code produces the following result, demonstrating backtracking after the exception handling, to the other choice points within the exceptional goal:
     ((no-exc 1)
      (no-exc 2)
      (caught 1 5)
      (caught 1 15)
      (no-exc 5))

The two ways of handling exceptions in non-deterministic programs are clearest to explain in Haskell terms, as two different ways to compose a non-determinism monad transformer such as ListT with an exception monad transformer such as Either err. (We use lists here only for the sake of example; strictly speaking, ListT is not fully a monad transformer.) Transforming an exception monad with ListT gives us the type Either err [a]. This type expresses either a list of choices Right [a] for the values of type a, or a definite exception Left err. This monad describes the ISO Prolog exception handling. The alternative is to transform the list monad with Either err, obtaining the type [Either err a] that expresses the list of choices for successful computations Right a and exceptions Left err, or the mixture of the two. Kanren implements a particular non-determinism monad LogicT. Transforming it with Either err is straightforward.

Hansei, a domain-specific probabilistic programming language embedded in OCaml, may be regarded as a logic programming system. Since OCaml has native exceptions, so does Hansei. Unlike Kanren, Hansei implements non-determinism directly, using the library of delimited continuations. Hansei supports both modes of exception handling, cutting choice points or preserving them. The direct-style implementation makes the difference lucid, reducing it to the dynamic scoping of an exception handler try relative to a `non-determinism handler' reify0. If try dynamically scopes over reify0, choice points are cut off. If an exception is caught and handled before it gets to reify0, choice points are preserved. (Different exceptions in Hansei may have different behavior with respect to choice points). Here is an illustration.

     open ProbM
     open Ptypes
     exception E of int
     let model () =
      let i = geometric 0.4 in
      if i = 3 || i = 4 then raise (E (100 + i)) else i
     (* val model : unit -> int = <fun> *)

The examples t1 and t2 below do the inference first. Since the geometric distribution is infinite, over the entire domain of natural numbers, we have to limit the depth of the exact inference over this model (see the first argument to reify_part). Once the inference extends far enough to trigger the exception, the inference is aborted. (The function reify_part is a composition of reify0 and the function to traverse the reified tree and collect the results. We can insert exception handling into reify_part so to preserve the values collected before an exception is raised.)

     type ('a,'b) either = Left of 'a | Right of 'b;;
     let t1 = try Right (reify_part (Some 2) model)
              with E x -> Left x
     (* Right [(0.4, 0); (0.24, 1)] *)
     let t2 = try Right (reify_part (Some 10) model)
              with E x -> Left x
     (* Left 103 *)

The alternative is to catch exceptions before reifying a non-deterministic computation. All choice points are preserved then.

     let t3 = reify_part (Some 10) (fun () -> try model () with E x -> x)
      val t3 : (Ptypes.prob * int) list =
        [(0.4, 0);  (0.24, 1);  (0.144, 2); (0.031, 5);  (0.019, 6);
         (0.01, 7); (0.007, 8); (0.004, 9); (0.086, 103); (0.052, 104)]
The current version is 1.0, June 2011.
exceptions.scm [7K]
Implementation of exceptions in Kanren, and their test cases

Logic programming in Hansei

Generators in Logic Programming
The application of choice-points--preserving exceptions.


leanTAP theorem prover in pure Prolog

leanTAP (Beckert and Posegga, 1995) is a simple, elegant and efficient theorem prover for the full classical first-order predicate logic. The prover is based on semantic tableaux.

The published leanTAP code has cuts in almost every clause of the prover and the converter to the negative normal form (NNF). Furthermore, both the prover and the NNF converter rely on copy_term/2 . Cut and copy_term/2 are extra-logical features and may lead to unsoundness, which is especially worrisome when writing a theorem prover. We would like to be sure of the code. There arises a problem of re-writing leanTAP in pure Prolog, in Horn-clause logic. The included code solves the problem.

The most difficult part is emulating copy_term/2 used when instantiating a universally quantified formula all(X,Fml) . LeanTAP uses free logic variables for variables of logic formulas, such as X above . When we instantiate the formula the logic variable becomes bound and cannot be re-bound. To be able to instantiate the universally-quantified formula many times, we have to make a clone all(Xnew,FmlNew) where Xnew is a fresh logic variable. The predicate split_inst/3 in the enclosed code manages the cloning in pure Prolog. The deterministic goal split_inst(F,F1,F2) unifies F1 and F2 with the copies of the input formula F . As we traverse F we instantiate logic variables with the term of the form w(Xnew1,Xnew2) containing two fresh variables. We can now distinguish what used to be a free variable in F from non-variable terms. Although that variable is no longer free, it is bound to the term containing two free variables Xnew1 and Xnew2 . As we traverse the formula, we remove the w(,) wrapper and obtain two copies of the formula, with independent and free variables. The following is the result of evaluating a sample cloning goal.

     ?- split_inst(all(X,all(Y,[p,X,Y,X])),R1,R2).
     X = w(_G319, _G322)
     Y = w(_G328, _G331)
     R1 = all(_G319, all(_G328, [p, _G319, _G328, _G319]))
     R2 = all(_G322, all(_G331, [p, _G322, _G331, _G322]))
The skolemizer relies on a similar trick to obtain the list of free variables in a formula. As we traverse binders such as all(X,F) we instantiate X -- with a special `quotation' term w1(Xnew) . The quotation marks let us distinguish former free variables. As we traverse the term and reconstruct it, we remove the quotation marks and recover free variables.

Our code assumes that bound variables in the original formula are denoted by distinct logic variables. Unlike the lambda-calculator, this invariant is preserved during the NNF normalization and proof search. Our logic is first order, and so variables could be instantiated with terms but not with formulas; only formulas may contain binding forms.

The current version is 1.2, Oct 31, 2008.
leanTAPpure.prl [10K]
Commented pure Prolog code, of the main prover prove/4 , the converter to the negative normal form nnf/3 , and the combined fullprove/2 . The code solves several Pelletier problems.

Bernhard Beckert and Joachim Posegga. leanTAP: Lean Tableau-based Deduction. Journal of Automated Reasoning, 15(3), 339-358 (1995).
< >


leanTAP theorem prover in Kanren

leanTAP (Beckert and Posegga, 1995) is a simple, elegant and efficient theorem prover for the full classical first-order predicate logic. The prover is based on semantic tableaux.

The miniKanren implementation uses higher-order abstract syntax, to avoid copy_term , and an advanced evaluator that removes the need for the explicit iterative deepening. The result is an even leaner prover.

The current version is 1.5, Aug 30, 2005.
< >

Bernhard Beckert and Joachim Posegga. leanTAP: Lean Tableau-based Deduction. Journal of Automated Reasoning, 15(3), 339-358 (1995).
< >

leanTAP theorem prover in pure Prolog


Minimization of a Finite Automaton

This Prolog code implements Hopcroft-Ullman Algorithm 2.6 to minimize a Finite Automaton. Given a set of states, the initial and the final state(s), the alphabet and the transition function, the code returns the list of equivalent states. The equivalent states can then be merged, resulting in a smaller Finite State Machine.
The current version is 1.0, October 1991.
minimizer.prl [7K]
Commented source code


Recursive Data Types in Prolog

This simple code exhibits two recursive data types:

We then demonstrate simple deep copying of a binary tree with optional modifications.

The current version is 1.0, June 1992.
RecursiveDatatypes.prl [3K]


Shortest Paths in a directed graph

A Modified Dijkstra algorithm to determine one-to-all shortest paths in a directed unweighted graph.

Since all edges have the same weight, an edge between two vertices is the shortest path between these vertices. Thus to find shortest paths from a given vertex to the others we merely need to do a breadth-first search.

This Prolog code takes advantage of Prolog's built-in ``database'' to maintain the queue of vertices for the breadth-first graph traversal.

The current version is 1.0, November 1991.
shortest_path_weight1.prl [4K]
Commented source code


Knight's tours

Given an NxN chess board and a knight standing at pos(Row,Col) , we should print out a sequence of knight's moves that pass through every cell on the board exactly once. The last cell of the tour may or may not be the same as the starting cell: the tour does not have to be closed.

The predicate knight_tour(N,Pos) tries to solve the open tour problem for the NxN board. The necessary condition for a solution is N*N-1 being divisible by three. Here is a sample run:

      found solution
      Board of 4 dim
      3:   8   7   6   5
      2:   9  10  11   4
      1:  14  13  12   3
      0:  15   0   1   2
The number in a cell tells that cell's position in a tour: the tour starts at the cell marked 0 and continues to the cells marked 1, 2, 3...15.

The code can be modified to print out all closed tours starting from a given position -- not necessarily complete tours of the board. The latter may exist only if N is divisible by 3 and is at least 6.

The code demonstrates an implementation of matrices in Prolog, as lists of lists. The code shows off ``updating'' of matrix elements and undoing the ``updates'' on back-tracking. These updates are all functional rather than destructive.

The current version is 1.0, September 1999.
Knight.prl [10K]
Commented source code

A web site dedicated to various Knight Tour problems and solutions
< >


N-queen problem

The problem is to position N queens on a N-by-N chessboard such that no queen beats the others. This introductory Prolog code produces all permutation of a given list and prints those that correspond to a safe position of the N queens.
The current version is 1.0, November 1993.
QueensProblem.prl [4K]
Commented source code

Last updated January 1, 2013

This site's top page is
Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML