Résumé:
L'algorithme de Staalmarck est un des plus efficaces pour verifier qu'une formule booleenne est une tautologie. Nous presentons et evaluons plusieurs methodes pour construire une tactique Coq utilisant cet algorithme.
Staalmarck's algorithm is one of the most efficient for checking that a boolean formula is a tautology. We present and evaluate several possible ways of building a Coq tactic that uses this algorithm.
Retour au sommaire / Back to schedule