GitHub - mkoconnor/John-Harrison-s-Automated-Reasoning-Code: This is a copy of John Harrison's automated reasoning code, with my personalizations

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 16 Commits
LICENSE.txt		LICENSE.txt
Makefile		Makefile
Mk_ml_file		Mk_ml_file
Quotexpander.ml		Quotexpander.ml
README		README
bdd.ml		bdd.ml
combining.ml		combining.ml
completion.ml		completion.ml
complex.ml		complex.ml
cong.ml		cong.ml
cooper.ml		cooper.ml
decidable.ml		decidable.ml
defcnf.ml		defcnf.ml
dp.ml		dp.ml
eqelim.ml		eqelim.ml
equal.ml		equal.ml
example.ml		example.ml
fol.ml		fol.ml
folderived.ml		folderived.ml
formulas.ml		formulas.ml
geom.ml		geom.ml
grobner.ml		grobner.ml
herbrand.ml		herbrand.ml
init.ml		init.ml
initialization.ml		initialization.ml
interpolation.ml		interpolation.ml
intro.ml		intro.ml
lcf.ml		lcf.ml
lcffol.ml		lcffol.ml
lcfprop.ml		lcfprop.ml
lib.ml		lib.ml
limitations.ml		limitations.ml
make.ml		make.ml
meson.ml		meson.ml
mktop.ml		mktop.ml
mktopml.ml		mktopml.ml
order.ml		order.ml
paramodulation.ml		paramodulation.ml
prolog.ml		prolog.ml
prop.ml		prop.ml
propexamples.ml		propexamples.ml
qelim.ml		qelim.ml
real.ml		real.ml
resolution.ml		resolution.ml
rewrite.ml		rewrite.ml
skolem.ml		skolem.ml
skolems.ml		skolems.ml
stal.ml		stal.ml
tableaux.ml		tableaux.ml
tactics.ml		tactics.ml
unif.ml		unif.ml

Repository files navigation

This is Michael O'Connor's "fork" of John Harrison's code accompanying his book 
"Handbook of Practical Logic and Automated Reasoning".  The license is the same 
as before, see LICENSE.TXT.

It has my personalizations. Right now, the changes are: running "make top" will
construct a proper custom toplevel with the appropriate libraries, and those 
libraries no longer have any side-effects when you link them in.