bagofN
! , 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.
Chung-chieh Shan. Slides of the talk at FLOPS08, April 14, 2008.
< http://www.cs.rutgers.edu/~ccshan/arithm/talk.pdf >
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.
(exists U. [U,U]) , and `common subexpression elimination' in logical programs. We draw parallels with effects, of creating logical variables.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.
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.
< http://soutei.sourceforge.net/ >
Version 2.1 of Soutei: the Haskell library and several sample applications
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).
insert(X,L,[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 .
var/1The 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
Yes
?- foo(1).
No
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.
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.
copy_term/2The 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).
Finally, cut, by itself expresses var/1:
noteq(X,X) :- !, fail.
noteq(_,_).
vr(X) :- (noteq(X,0), !, fail); (noteq(X,1), !, fail); true.
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.
< http://www.cs.ucla.edu/~zaniolo/papers/pruning.pdf >
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.
< http://www.cs.ucla.edu/~zaniolo/papers/jcss01.pdf >
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.
< http://reports-archive.adm.cs.cmu.edu/anon/2000/CMU-CS-00-175.pdf >
``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.''
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).
eval(E,E).
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)),
eval(Body,R).
eval(E,E).
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(C,Cout,[(X,Xnew)|Env],Body,BodyNew).
alpha_convert(Cin,Cin,[(v(C),Xnew)|_],v(C),Xnew).
alpha_convert(Cin,Cin,[(v(C1),_)|T],v(C),R) :-
uneq(C1,C), alpha_convert(Cin,Cin,T,v(C),R).
alpha_convert(Cin,Cin,_,c(T),c(T)).
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).
eval(E,E).
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(...) .
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)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.''throw(+Exception)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)
(catch
(fresh (x)
(conde
(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)]
*)
Generators in Logic Programming
The application of choice-points--preserving exceptions.
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.
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).
< http://citeseer.ist.psu.edu/beckert95leantap.html >
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.
Bernhard Beckert and Joachim Posegga. leanTAP: Lean Tableau-based Deduction. Journal of Automated Reasoning, 15(3), 339-358 (1995).
< http://citeseer.ist.psu.edu/beckert95leantap.html >
nat = {zero} + nat with the operation plusbtree = {integer} + (btree * btree)We then demonstrate simple deep copying of a binary tree with optional modifications.
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.
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:
knight_tour(4,pos(0,1)).
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.
A web site dedicated to various Knight Tour problems and solutions
< http://www.borderschess.org/KnightTour.htm >
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.oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML