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
Dedam: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses
efficient full higher order unification zipperposition