References

  1. 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.
  2. 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.
  3. Haniel Barbosa, Jasmin Christian Blanchette & Pascal Fontaine (2017): Scalable Fine-Grained Proofs for Formula Processing. Research Report. Inria, doi:10.1007/978-3-319-63046-5_25. Available at https://hal.inria.fr/hal-01526841.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org