package coq-stalmarck

  1. Overview
  2. Homepage
Verified implementation of Stålmarck's algorithm for proving tautologies in Coq

Install

Dune Dependency

Authors

Maintainers

Sources

v8.16.0.tar.gz
sha512=ebe1f79da3c8a45189e51f856d24b3faee7ea14529f3598b733058b93639a6a845352937bf58ed04736825ad63aa5e1ad1cf04f3594ee414474f1a2707c52d6a

Description

A two-level approach to prove tautologies using Stålmarck's algorithm in Coq.

Dependencies (1)

  1. coq >= "8.16" & < "8.17~"

Dev Dependencies

None

Used by (1)

  1. coq-stalmarck-tactic = "8.16.0"

Conflicts

None

Rocq

Interactive Theorem Prover