### Abstract

[Sch18] Anders Schlichtkrull. "Formalization of the
Resolution Calculus for First-Order Logic". Journal of Automated
Reasoning, 2018.

[Sch16] Anders
Schlichtkrull. "Formalization of the Resolution Calculus for First-Order
Logic". In: ITP 2016. Vol. 9807. LNCS. Springer, 2016.

[Sch15] Anders Schlichtkrull.
"Formalization of Resolution Calculus in Isabelle".
https://people.compute.dtu.dk/andschl/Thesis.pdf.
MSc thesis. Technical University of Denmark, 2015.

[BA12] Mordechai Ben-Ari. *Mathematical Logic for
Computer Science*. 3rd. Springer, 2012.

[CL73] Chin-Liang Chang and Richard Char-Tung Lee.
*Symbolic Logic and Mechanical Theorem Proving*. 1st. Academic
Press, Inc., 1973.

[Lei97] Alexander
Leitsch. *The Resolution Calculus*. Texts in theoretical computer
science. Springer, 1997.

[IsaFoL]
IsaFoL authors.
IsaFoL: Isabelle Formalization of Logic.
https://bitbucket.org/jasmin_blanchette/isafol.

### License

### History

- March 20, 2018
- added a concrete instance of the unification and completeness theorems using the First-Order Terms AFP-entry from IsaFoR as described in the papers
- January 24, 2018
- added several new versions of the soundness and completeness theorems as described in the paper