Source Archive
Version 1.0, 20.11.2000.

M. Ben-Ari
Mathematical Logic for Computer Science
Second Edition.
Springer-Verlag London, 2001.

Copyright 2000. M. Ben-Ari.
Copying and modification is permitted for
personal and academic research and teaching.
Commercial and/or for-profit use is permitted
only by permission of the author.

Email: moti.ben-ari@weizmann.ac.il
Web:   http://stwww.weizmann.ac.il/g-cs/benari/books.htm#ml2

The programs were developed on SWI-Prolog version 3.4.2,
which is a free implementation which runs on many platforms.
The software may be downloaded from:

http://www.swi.psy.uva.nl/projects/SWI-Prolog

The source archive is a zip file structured into directories:

common - common modules and files used by other programs
prop   - propositional calculus
bdd    - binary decision diagrams
pred   - predicate calculus
lp     - logic programming
tl     - temporal logic

For each program p.pl, there is a file p-t.pl
which contains test programs.
The programs use the predicate file_search_path
to access the common modules in the common directory,
so maintain the relative directory structure.

List of files:

Directory common:
ops.pl      - declaration of operators with precedence and associativity.
def.pl      - correspondance between symbols and internal operators.
            - semantic definition of Boolean operators.
intext.pl   - conversion from external to internal format and conversely.
io.pl       - display procedures for all programs (except BDDs).
cnf.pl      - conversion of a formula to CNF
            - (both propositional and predicate calculus).

Directory prop:   (propositional calculus)
tt.pl       - truth tables.
tabl.pl     - semantic tableaux.
systab.pl   - systematic semantic tableaux.
            - note: tabl and systab share a test program tabl-t.pl.
check.pl    - Hilbert proof checker.
resolv.pl   - resolution.

Directory bdd:    (binary decision diagrams)
bdd.pl      - BDD algorithms.
bddwrite.pl - display of BDDs.

Directory pred:   (predicate calculus)
tabl.pl     - semantic tableaux.
check.pl    - Hilbert proof checker.
skolem.pl   - skolemize a formula.
unify.pl    - unification algorithm.
resolv.pl   - resolution.
utility.pl  - procedures common to more than one file.

Directory lp:     (logic programming)
queen.pl    - eight-queens problem.
queen1.pl   - eight-queens problem (smart generation of configurations).

Directory tl:     (temporal logic)
tl.pl       - semantic tableaux .
peter.pl    - state diagram for Peterson's algorithm.
sym.pl      - symbolic model checking.