Formalizing Stalmarck's algorithm in Coq

Pierre Letouzey (1) , Laurent Théry (1)

1 CROAP - Design and Implementation of Programming Tools

We present the development of a machine-checked implementation of Stalmarck's algorithm. First, we prove the correctness and the completeness of an abstract representation of the algorithm. Then, we give an effective implementation of the algorithm that we prove correct.

Mots clés: stalmarck; boolean decision procedure; tautology; Coq; certified algorithm; extraction

Domaines: Logique en informatique [cs.LO]

Pierre Letouzey, Laurent Théry. Formalizing Stalmarck's algorithm in Coq. Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, 2000, Portland, United States. pp.388. ⟨hal-00150915⟩