See also notes on:

Automated Deduction in Equational Logic and Cubic Curves

  • Zipperposition

  • Sledgehammer

  • Idea: Convert resolution proof to bus proofs tree. Is this even possible or desirable?

Schulz teaching automated theorem proving polymorphic vampire

An Impossible Asylum - ATP checking of Smullyan puzzle found hypotheses inconsistent

Phillips & Stanovsky https://www2.karlin.mff.cuni.cz/~stanovsk/math/slides_esarm.pdf loop theory and non associative lagerbas https://www2.karlin.mff.cuni.cz/~stanovsk/math/slides_lpar08.pdf

Searching for a Fixed Point Combinators by Using Automated Theorem Proving: A Preliminary Report

Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs

tptp bibiography. It’s insane how much work is here

geometric database horn clauses.

Waldmeister and Twee - UEQ

REDUCING HIGHER-ORDER THEOREM PROVING TO A SEQUENCE OF SAT PROBLEMS

vampire and the fool

Dedam: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses

efficient full higher order unification zipperposition