handbook-of-practical-logic-and-automated-reasoning

Code from John Harrison's "Handbook of Practical Logic and Automated Reasoning"

Name		Name	Last commit message	Last commit date
Latest commit History 3 Commits
.gitignore		.gitignore
LICENSE.txt		LICENSE.txt
Makefile		Makefile
Mk_ml_file		Mk_ml_file
Quotexpander.ml		Quotexpander.ml
README.md		README.md
atp_interactive.ml		atp_interactive.ml
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
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

Provide feedback