!, 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.
As an example, our mul(X,Y,Z) can be used to multiply two numbers X
and Y -- or to find all factorizations of Z, or to check
divisibility. The predicate can also generate all triples of numbers
related by multiplication. The predicate div/4 can find all numbers
that divide the given one, perhaps unevenly, with the given quotient.
One can use log/4 to exponentiate, to find discrete logarithms or
roots.
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 may seem straightforward: apply var/1
to determine which of the arguments of, say, the add
predicate are instantiated, and use addition, subtraction,
or number generation as appropriate. However, var/1 is not a logical
predicate; it is also unsound, in general. 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 with just `pure logic'.
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.
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.
doi:10.1007/978-3-540-78969-7_7
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.
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.
Joint work with Andrew Pimlott.
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.
doi:10.1007/11737414
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:
each of negation, copy_term/2,
and cut by themselves 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(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
However, if we try to verify the answer and check if indeed foo(1)
is derivable from the current knowledge, we get:
?- foo(1).
No
With var/1, logic programming becomes programming in
inconsistent logic. We cannot generally trust any results.
\+/1 is just as
dangerous as var/1. Indeed, negation can express var/1 in one line:
vr(X) :- \+ \+ (X=0), \+ \+ (X=1).Only an unbound 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/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).
var/1:
noteq(X,X) :- !, fail.
noteq(_,_).
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, statically assuring
the condition is not decidable.
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.''
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 the result of its
reduction.
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. At that moment all
occurrences of X in the Body of the abstraction get 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?
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 :types.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)]
*)
exceptions.scm [7K]
Implementation of exceptions in Kanren, and their test cases
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.
leanTAPpure.prl [10K]
Commented pure Prolog code: 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).
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.
leanTAP.scm [18K]
The mini-Kanren code
Bernhard Beckert and Joachim Posegga. leanTAP: Lean Tableau-based Deduction. Journal of Automated Reasoning, 15(3), 339-358 (1995).
minimizer.prl [7K]
Commented source code
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.
Knight.prl [10K]
Commented source code
N queens on a
NxN 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 queens.
QueensProblem.prl [4K]
Commented source code