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 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