AVATAR: the architecture for first-order theorem provers, CAV 2014, pp.696-710, 2014. ,
Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, 2012. ,
Learning-assisted automated reasoning with Flyspeck, Journal of Automated Reasoning, vol.53, issue.2, 2014. ,
E -a brainiac theorem prover, AI Commun, vol.15, 2002. ,
Vampire 1.1 (system description), Proceedings of the First International Joint Conference on Automated Reasoning, IJCAR '01, pp.376-380, 2001. ,
System Description: SPASS Version 3.0, Lecture Notes in Computer Science, vol.4603, pp.514-520, 2007. ,
On Restrictions of Ordered Paramodulation with Simplification, 10th International Conference on Automated Deduction ,
, Lecture Notes in Computer Science, vol.449, pp.427-441, 1990.
Coming to terms with quantified reasoning, pp.260-270, 2017. ,
ACL2: An industrial strength version of Nqthm, pp.23-34, 1996. ,
The Karlsruhe induction theorem proving system, International Conference on Automated Deduction, pp.672-674, 1986. ,
A unified view of induction reasoning for first-order logic, The Alan Turing Centenary Conference, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00763236
Induction for SMT solvers, Verification, Model Checking, and Abstract Interpretation (VMCAI), 2015. ,
Combining superposition and induction: A practical realization, Frontiers of Combining Systems, vol.8152, pp.7-22, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00934610
Otter-lambda, a Theorem-prover with Untyped Lambda-unification, Proceedings of the Workshop on Empirically Successful First Order Reasoning, 2nd International Joint Conference on Automated Reasoning, 2004. ,
Automatic Induction inside Superposition, 2017. ,
Splitting Without Backtracking, 2001. ,
TIP: Tons of Inductive Problems, Conferences on Intelligent Computer Mathematics, pp.333-337, 2015. ,
Rippling: A heuristic for guiding inductive proofs, Artificial Intelligence, vol.62, issue.2, pp.185-253, 1993. ,
A Computational Logic Handbook: Formerly Notes and Reports in, Computer Science and Applied Mathematics, 2014. ,
Lemma discovery in automating induction, pp.538-552, 1996. ,
Strategies for mechanizing structural induction, IJCAI, 1977. ,
Theorem Proving Modulo, Journal of Automated Reasoning, 2003. ,
URL : https://hal.archives-ouvertes.fr/inria-00077199
Embedding Deduction Modulo into a Prover, pp.155-169, 2010. ,
, The Satisfiability Modulo Theories Library (SMT-LIB), 2016.
Hierarchic superposition with weak abstraction, Automated Deduction-CADE-24, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00931919
A decision procedure for (co)datatypes in SMT solvers, LNCS, vol.9195, pp.197-213, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01397082
An abstract decision procedure for satisfiability in the theory of inductive data types, J. Satisf. Boolean Model. Comput, vol.3, pp.21-46, 2007. ,
Z3: An efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, vol.4963, pp.337-340, 2008. ,
Superposition for fixed domains, ACM Transactions on Computational Logic (TOCL), vol.11, issue.4, p.27, 2010. ,
A mechanizable induction principle for equational specifications, 9th International Conference on Automated Deduction, vol.310, pp.162-181, 1988. ,
Hipspec: Automating inductive proofs of program properties, ATx/WInG@ IJCAR, 2012. ,
Smallcheck and lazy smallcheck: automatic exhaustive testing for small values, Acm sigplan notices, vol.44, pp.37-48, 2008. ,
QuickCheck: a lightweight tool for random testing of Haskell programs, Acm sigplan notices, vol.46, issue.4, pp.53-64, 2011. ,
Property directed generation of first-order test data, Trends in Functional Programming, pp.105-123, 2007. ,
Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond, 2015. ,
URL : https://hal.archives-ouvertes.fr/tel-01223502
The Vampire and the FOOL, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pp.37-48, 2016. ,
The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, Journal of Automated Reasoning, vol.43, issue.4, pp.337-362, 2009. ,
Conjecture Synthesis for Inductive Theories, Journal of Automated Reasoning, 2010. ,