Leo Bachmair & Harald Ganzinger (1994):
Rewrite-Based Equational Theorem Proving with Selection and Simplification.
Journal of Logic and Computation 4(3),
pp. 217–247,
doi:10.1093/logcom/4.3.217.
Haniel Barbosa, Jasmin Christian Blanchette & Pascal Fontaine (2017):
Scalable Fine-Grained Proofs for Formula Processing.
In: Leonardo de Moura: Conference on Automated Deduction (CADE),
LNCS 10395.
Springer,
pp. 398–412,
doi:10.1007/978-3-319-63046-5_25.
Haniel Barbosa, Pascal Fontaine & Andrew Reynolds (2017):
Congruence Closure with Free Variables.
In: Axel Legay & Tiziana Margaria: Tools and Algorithms for Construction and Analysis of Systems (TACAS),
LNCS 10206,
pp. 214–230,
doi:10.1007/978-3-662-54580-5_13.
Clark Barrett, Pascal Fontaine & Cesare Tinelli (2015):
The SMT-LIB Standard: Version 2.5.
Technical Report.
Department of Computer Science, The University of Iowa.
Available at www.SMT-LIB.org.
Frédéric Besson, Pascal Fontaine & Laurent Théry (2011):
A Flexible Proof Format for SMT: a Proposal.
In: Pascal Fontaine & Aaron Stump: Workshop on Proof eXchange for Theorem Proving (PxTP).
Available at https://hal.inria.fr/hal-00642544.
Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka & Albert Steckermeier (2016):
Semi-intelligible Isar Proofs from Machine-Generated Proofs.
Journal of Automated Reasoning 56(2),
pp. 155–200,
doi:10.1007/s10817-015-9335-3.
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson & Josef Urban (2016):
Hammering towards QED.
Journal of Formalized Reasoning 9(1),
pp. 101–148,
doi:10.6092/issn.1972-5787/4593.
Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe & Pascal Fontaine (2009):
veriT: An Open, Trustable and Efficient SMT-Solver.
In: Renate A. Schmidt: Conference on Automated Deduction (CADE),
LNCS 5663.
Springer,
pp. 151–156,
doi:10.1007/978-3-642-02959-2_12.
Gabriel Ebner, Stefan Hetzl, Giselle Reis, Martin Riener, Simon Wolfsteiner & Sebastian Zivota (2016):
System Description: GAPT 2.0.
In: Nicola Olivetti & Ashish Tiwari: International Joint Conference on Automated Reasoning (IJCAR),
LNCS 9706.
Springer,
pp. 293–301,
doi:10.1007/978-3-319-40229-1_20.
Robert Nieuwenhuis, Albert Oliveras & Cesare Tinelli (2006):
Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam–Logemann–Loveland Procedure to DPLL(T).
Journal of the ACM 53(6),
pp. 937–977,
doi:10.1145/1217856.1217859.
Robert Nieuwenhuis & Albert Rubio (2001):
Paramodulation-Based Theorem Proving.
In: Alan Robinson & Andrei Voronkov: Handbook of Automated Reasoning I,
pp. 371–443,
doi:10.1016/B978-044450813-3/50009-6.
Dan Rosén & Nicholas Smallbone (2015):
TIP: Tools for Inductive Provers.
In: Martin Davis, Ansgar Fehnker, Annabelle McIver & Andrei Voronkov: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR).
Springer,
pp. 219–232,
doi:10.1007/978-3-662-48899-7_16.