概述

1. Handbook of Automated Reasoning (Chapter 2, 7) 2001
2. Handbook of Practical Logic and Automated Reasoning(Chapter 3) Harrison, John 2009

系统介绍

1. CAV

   First-Order Theorem Proving and Vampire Kovács, Laura, and Voronkov, Andrei In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 2013
2. LPAR

   System Description: E 1.8 Schulz, Stephan In Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings 2013

算法验证

1. CADE

   Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover Schlichtkrull, Anders, Blanchette, Jasmin Christian, Traytel, Dmitriy, and Waldmann, Uwe In Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings 2018
2. CADE

   A Comprehensive Framework for Saturation Theorem Proving Waldmann, Uwe, Tourret, Sophie, Robillard, Simon, and Blanchette, Jasmin In Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I 2020

高阶逻辑的扩展

机器学习引导证明

1. LPAR

   Deep Network Guided Proof Search Loos, Sarah M., Irving, Geoffrey, Szegedy, Christian, and Kaliszyk, Cezary In LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017 2017
2. CADE

   Monte Carlo Tableau Proof Search Färber, Michael, Kaliszyk, Cezary, and Urban, Josef In Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings 2017
3. ITP

   ProofWatch: Watchlist Guidance for Large Theories in E Goertzel, Zarathustra, Jakubuv, Jan, Schulz, Stephan, and Urban, Josef In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings 2018