package coq-stalmarck
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.
Tags
category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:boolean formula keyword:tautology checker logpath:Stalmarck.Algorithm date:2022-09-16Published: 17 Sep 2022
Dependencies (1)
-
coq
>= "8.16" & < "8.17~"
Dev Dependencies
None
Used by (1)
-
coq-stalmarck-tactic
= "8.16.0"
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page