Computers and Automata (1953)
fermatslibrary.com
fermatslibrary.com
Now that is a curious puzzle in the sense that I can't think how to express it in Prolog. You'd need to assert the truth of assertions which implies quantifying over assertions, and Prolog doesn't allow that. I'm sure I'm making this much more complex than it need be, there has to be a much more straightforward way, any ideas please?
In Prolog, we can express these relations with CLP(B), constraint logic programming over Boolean variables:
?- use_module(library(clpb)).
true.
?- sat(G),
sat(E),
sat(C =:= ~D),
sat(A =:= (B =:= (C =:= (D =:= (E =:= (F =:= ~G)))))),
sat(~A),
labeling([A,B,C,D,E,F,G]).
Yielding 4 solutions that satisfy all constraints: G = 1, E = 1, C = 0, D = 1, A = 0, B = 0, F = 1
; G = 1, E = 1, C = 0, D = 1, A = 0, B = 1, F = 0
; G = 1, E = 1, C = 1, D = 0, A = 0, B = 0, F = 1
; G = 1, E = 1, C = 1, D = 0, A = 0, B = 1, F = 0.
From this, it is clear that there are 3 engineers, in all possible situations consistent with the description.If we omit the labeling/1 goal which enumerates all solutions, then we get a symbolic representation of all remaining constraints:
G = 1, E = 1, A = 0, clpb:sat(C=:=D#B#F), clpb:sat(C=\=D).
From this, it is clear that there are at least 2 engineers in every solution: A (as stated in the description of the puzzle), and either C or D (but not both).Tested with Scryer Prolog.
The thing I find especially interesting about these sorts of puzzles is the translation from the word problem to the logical formalism. It seems like a separate domain from solving the problem itself.
For instance, in this concrete case, with a suitable operator definition for the operator says, we can write:
:- op(800, xfy, says).
solution([A,B,C,D,E,F,G]) :-
G = salesman,
E = salesman,
C says D = engineer,
A = engineer,
A says B says C says D says E says F says G = engineer.
It is then left to interpret the statements, which we can do for example with: :- use_module(library(dif)).
engineer says Stmt :- false(Stmt).
salesman says Stmt :- true(Stmt).
false(A = B) :- dif(A, B).
false(engineer says Stmt) :- true(Stmt).
false(salesman says Stmt) :- false(Stmt).
true(A = A).
true(engineer says Stmt) :- false(Stmt).
true(salesman says Stmt) :- true(Stmt).
Yielding: ?- solution(S).
S = [engineer,engineer,engineer,salesman,salesman,salesman,salesman]
; S = [engineer,salesman,engineer,salesman,salesman,engineer,salesman]
; S = [engineer,engineer,salesman,engineer,salesman,salesman,salesman]
; S = [engineer,salesman,salesman,engineer,salesman,engineer,salesman]
; false.Since they don't have Apache configured to hide directory listings, there's a whole trove of scans and other material listed at <https://webmuseum.mit.edu/files/>.
McCallum D. B. and Smith J. B.. Mechanized reasoning—logical computers and their design.
I can only find a review of it. This is an area of interest for me as I want to design educational logic machines to teach proofs.
Contact them and ask
https://annas-archive.org/md5/c50b9ec404b79e6a7d6ad77e9ef55f...
Front matter:
https://annas-archive.org/md5/e9080f059fa914cc7ae31e2790b267...