Automated Theorem Proving
See also notes on:
 SMT
 prolog

datalog
 https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324010/ Teaching Automated Theorem Proving by Example: PyRes 1.2
 https://logictools.org/ neat online ATP interface
 TPTP
 Vampire
 E Prover
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 TheoremProving Programs
tptp bibiography. Itâ€™s insane how much work is here
geometric database horn clauses.
Waldmeister and Twee  UEQ
REDUCING HIGHERORDER THEOREM PROVING TO A SEQUENCE OF SAT PROBLEMS
Dedam: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses
efficient full higher order unification zipperposition