package logtk
Core types and algorithms for logic
Install
Dune Dependency
Authors
Maintainers
Sources
1.6.tar.gz
md5=97cdb2f90468e9e27c7bbe3b4fb160bb
sha512=fee73369f673a91dfa9e265fc69be08b32235e10a495f3af6477d404fcd01e3452a0d012b150f3d7f97c00af2f6045019ad039164bf698f70d771231cc4efe5d
doc/logtk.proofs/Logtk_proofs/LLProver/index.html
Module Logtk_proofs.LLProverSource
Low Level Prover
A small theorem prover that checks entailment of ground formulas, with higher order terms and some theories
Is this set of tags accepted by the tableau prover?
prove a b returns R_ok if a => b is a tautology.
On This Page