19 search results for "tag:"category:Mathematics/Logic""
-
coq-color
No documentation
A library on rewriting theory and terminationdate:2023-06-28 logpath:CoLoR category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category:Computer Science/Data Types and Data Structures category:Computer Science/Lambda Calculi category:Mathematics/Algebra category:Mathematics/Combinatorics and Graph Theory category:Mathematics/Logic/Type theory category:Miscellaneous/Extracted Programs/Type checking unification and normalization keyword:rewriting keyword:termination keyword:lambda calculus keyword:list keyword:multiset keyword:polynomial keyword:vectors keyword:matrices keyword:FSet keyword:FMap keyword:term keyword:context keyword:substitution keyword:universal algebra keyword:varyadic term keyword:string keyword:alpha-equivalence keyword:de Bruijn indices keyword:simple types keyword:matching keyword:unification keyword:relation keyword:ordering keyword:quasi-ordering keyword:lexicographic ordering keyword:ring keyword:semiring keyword:well-foundedness keyword:noetherian keyword:finitely branching keyword:dependent choice keyword:infinite sequences keyword:non-termination keyword:loop keyword:graph keyword:path keyword:transitive closure keyword:strongly connected components keyword:topological ordering keyword:rpo keyword:horpo keyword:dependency pair keyword:dependency graph keyword:semantic labeling keyword:reducibility keyword:Girard keyword:fixpoint theorem keyword:Tarski keyword:pigeon-hole principle keyword:Ramsey theorem1.8.5CeCILL-2.1Used by 0 other packages16 Apr 2024 -
coq-comp-dec-modal
No documentation
Constructive proofs of soundness and completeness for K, K*, CTL, PDL, and PDL with converse1.2CECILL-BUsed by 0 other packages24 Jul 2024 -
coq-coqrel
No documentation
Binary logical relations library for the Coq proof assistant0.1.0MITUsed by 0 other packages27 Jan 2017 -
coq-gaia
No documentation
Implementation of books from Bourbaki's Elements of Mathematics in Coq1.13MITUsed by 1 other packages30 Oct 2021 -
coq-gaia-hydras
No documentation
Bridge in Coq between Gaia and Hydra battles0.9MITUsed by 0 other packages25 May 2022 -
coq-gaia-ordinals
No documentation
Implementation and properties of ordinals in Coq using Mathematical Components2.2MITUsed by 1 other packages11 Aug 2024 -
coq-gaia-theory-of-sets
No documentation
Implementation of the Theory of Sets from Bourbaki's Elements of Mathematics in Coq2.2MITUsed by 2 other packages11 Aug 2024 -
coq-generic-environments
No documentation
Generic Environments is a library that provides an abstract data type for environments8.11.0MITUsed by 0 other packages26 Oct 2020 -
coq-goedel
No documentation
Coq proof of the Gödel-Rosser 1st incompleteness theorem8.13.0MITUsed by 0 other packages10 Aug 2021 -
coq-hoare-tut
No documentation
A Tutorial on Reflecting in Coq the generation of Hoare proof obligations8.11.1LGPL-3.0-or-laterUsed by 0 other packages05 Jun 2020 -
coq-hydra-battles
No documentation
Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq0.9MITUsed by 2 other packages25 May 2022 -
coq-inconsequential_modus_ponens
No documentation
A Coq library about how redundant modus ponens is1.0.6CC-BY-SA-3.0Used by 0 other packages25 Sep 2022 -
coq-mathcomp-classical
No documentation
A library for classical logic for mathematical components1.8.0CECILL-CUsed by 2 other packages19 Dec 2024 -
coq-mk-reals-axioms
No documentation
A Coq formalization of the axiomatic definition of real numbers1.0.0LGPL-2.1-onlyUsed by 0 other packages28 Aug 2024 -
coq-morse-kelley-axiomatic-set-theory
No documentation
A Coq formalization of the Morse-Kelley axiomatic set theory1.0.0LGPL-2.1Used by 0 other packages24 Jul 2024 -
coq-ordinal
No documentation
Ordinal Numbers in Coq0.5.4MITUsed by 0 other packages18 Dec 2024 -
coq-paco
No documentation
Coq library implementing parameterized coinduction4.2.2BSD-3-ClauseUsed by 3 other packages31 Dec 2024 -
coq-yalla
No documentation
Yalla library2.0.6LGPL-3.0-or-laterUsed by 0 other packages16 Sep 2024 -
coq-zorns-lemma
No documentation
This library develops some basic set theory in Coq10.2.0LGPL-2.1-or-laterUsed by 1 other packages21 Aug 2023