
@article{schlichtkrull2018,
	Author = {Schlichtkrull, Anders},
	Journal = {Journal of Automated Reasoning},
	Title = {Formalization of the Resolution Calculus for First-Order Logic},
	Publisher = {Springer},
	Year = {2018}}

@url{isafor,
	Author = {Sternagel, Christian and Thiemann, Ren{\'e}},
	Howpublished = {\url{http://cl-informatik.uibk.ac.at/software/ceta/}},
	Title = {An {Isabelle/HOL} formalization of rewriting for certified termination analysis}}

@url{unify,
	Author = {Schlichtkrull, Anders},
	Howpublished = {\url{https://bitbucket.org/jasmin_blanchette/isafol/src/master/Unordered_Resolution/}},
	Title = {Formalization of First-Order Unordered Resolution}}

@book{leitsch,
	Author = {Alexander Leitsch},
	Publisher = {Springer},
	Series = {Texts in theoretical computer science},
	Title = {The Resolution Calculus},
	Year = {1997}}

@book{chang,
	Address = {Orlando, FL, USA},
	Author = {Chang, Chin-Liang and Lee, Richard Char-Tung},
	Edition = {1st},
	Publisher = {Academic Press, Inc.},
	Title = {Symbolic Logic and Mechanical Theorem Proving},
	Year = {1973}}

@book{ben-ari,
	Author = {Ben-Ari, Mordechai},
	Edition = {3rd},
	Publisher = {Springer},
	Title = {Mathematical Logic for Computer Science},
	Year = {2012}}

@url{isafol,
	Author = {{IsaFoL authors}},
	Howpublished = {\url{https://bitbucket.org/isafol/isafol}},
	Title = {{I}sa{F}o{L}: {Isabelle} {Formalization} of {Logic}}}

@mastersthesis{thesis,
	Author = {Schlichtkrull, Anders},
	Note = {\url{https://people.compute.dtu.dk/andschl/Thesis.pdf}},
	School = {Technical University of Denmark},
	Title = {Formalization of Resolution Calculus in {Isabelle}},
	Type = {MSc thesis},
	Year = {2015}}

@inproceedings{schlichtkrull2016,
	Author = {Schlichtkrull, Anders},
	Booktitle = {ITP 2016},
	Publisher = {Springer},
	Series = {LNCS},
	Title = {Formalization of the Resolution Calculus for First-Order Logic},
	Volume = {9807},
	Year = {2016}}
