7 search results for "tag:"category: Mathematics/Logic/Foundations""

Showing 1 - 7
  1. coq-classical-realizability

    No documentation

    Krivine's classical realizability
    keyword: classical realizability keyword: Krivine's realizability keyword: primitive datatype keyword: non determinism keyword: quote keyword: axiom of countable choice keyword: real numbers category: Mathematics/Logic/Foundations
    Lionel Rieg <lionel.rieg@ens-lyon.org>
    8.10.0
    BSD
    Used by 0 other packages
    19 Oct 2020
  2. coq-ipc

    No documentation

    Intuitionistic Propositional Checker
    keyword: intuitionistic logic keyword: proof search keyword: proof-as-programs keyword: correct-by-construction keyword: program verification keyword: program extraction category: Mathematics/Logic/Foundations category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category: Miscellaneous/Extracted Programs/Decision procedures
    Klaus Weich
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  3. coq-lesniewski-mereology

    No documentation

    Knowledge-based Dependently Typed Language (KDTL)
    keyword: mereology keyword: protothetic keyword: ontology keyword: nominalist theory keyword: extensionality category: Mathematics/Logic/Foundations
    Richard Dapoigny <richard.dapoigny@univ-savoie.fr> [https://www.researchgate.net/profile/Richard_Dapoigny] Patrick Barlatier <patrick.barlatier@univ-savoie.fr> [https://www.researchgate.net/profile/Patrick_Barlatier]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  4. coq-paradoxes

    No documentation

    Paradoxes in Set Theory and Type Theory
    keyword: Reynolds paradox keyword: Burali-Forti paradox keyword: Diaconescu paradox keyword: set theory keyword: system U keyword: inconsistency keyword: Hurkens paradox category: Mathematics/Logic/Foundations
    Bruno Barras Thierry Coquand Hugo Herbelin Benjamin Werner
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  5. coq-presburger

    No documentation

    Presburger's algorithm
    keyword: integers keyword: arithmetic keyword: decision procedure keyword: Presburger category: Mathematics/Logic/Foundations category: Mathematics/Arithmetic and Number Theory/Miscellaneous category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures date: March 2002
    Laurent Théry
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  6. coq-prfx

    No documentation

    Proof Reflection in Coq
    keyword: first-order logic keyword: natural deduction keyword: reflection keyword: proof terms keyword: de Bruijn indices keyword: permutative conversions category: Mathematics/Logic/Foundations date: 15 April 2005
    Dimitri Hendriks <hendriks@cs.ru.nl> [http://www.cs.ru.nl/~hendriks/]
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  7. coq-propcalc

    No documentation

    Propositional Calculus
    keyword: propositional calculus keyword: classical logic keyword: completeness keyword: natural deduction keyword: sequent calculus keyword: cut elimination category: Mathematics/Logic/Foundations
    Floris van Doorn <fpvdoorn@gmail.com> [http://www.contrib.andrew.cmu.edu/~fpv/]
    8.10.0
    BSD
    Used by 0 other packages
    07 Dec 2019