24 search results for "tag:"category: Mathematics/Logic""

Showing 1 - 24
  1. coq-cantor

    No documentation

    On Ordinal Notations
    keyword: ordinal numbers keyword: well-foundedness keyword: termination keyword: rpo keyword: Goodstein sequences category: Mathematics/Logic category: Mathematics/Arithmetic and Number Theory/Number theory date: 2006-05-22
    Pierre Castéran <pierre.casteran@labri.fr> [http://www.labri.fr/~casteran/] Évelyne Contejean <contejea@lri.fr> [http://www.lri.fr/~contejea]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  2. coq-cats-in-zfc

    No documentation

    Category theory in ZFC
    keyword: set theory keyword: ordinal numbers keyword: cardinal numbers keyword: category theory keyword: functors keyword: natural transformation keyword: limit keyword: colimit category: Mathematics/Logic/Set theory category: Mathematics/Category Theory date: 2004-10-10
    Carlos Simpson <carlos@math.unice.fr> [http://math.unice.fr/~carlos/]
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  3. coq-cds4ltl

    No documentation

    A Calculational Deductive System for Linear Temporal Logic
    keyword: temporal logic category: Mathematics/Logic/Modal logic date: 2022-07-23 logpath: CDS4LTL
    John Wiegley
    1.0.0
    BSD-3-Clause
    Used by 0 other packages
    23 Jul 2022
  4. 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
  5. coq-coq-in-coq

    No documentation

    A formalisation of the Calculus of Construction
    keyword: calculus of constructions category: Mathematics/Logic/Type theory category: Miscellaneous/Extracted Programs/Type checking unification and normalization
    Bruno Barras
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  6. coq-ctltctl

    No documentation

    Computation Tree Logic for Reactive Systems and Timed Computation Tree Logic for Real Time Systems
    keyword: CTL keyword: TCTL keyword: real time keyword: reactive systems keyword: temporal logic keyword: timed automatas keyword: timed graphs keyword: discrete time keyword: modal logic category: Mathematics/Logic/Modal logic date: February-March 2000
    Carlos Daniel Luna
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  7. coq-functions-in-zfc

    No documentation

    Functions in classical ZFC
    keyword: set theory keyword: Zermelo-Fraenkel keyword: functions category: Mathematics/Logic/Set theory date: April 2001
    Carlos Simpson <carlos@math.unice.fr>
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  8. coq-higman-nw

    No documentation

    A program from an A-translated impredicative proof of Higman's Lemma
    keyword: A-translation keyword: Higman's lemma keyword: impredicativity keyword: System F keyword: extraction category: Mathematics/Logic category: Mathematics/Combinatorics and Graph Theory category: Miscellaneous/Extracted Programs/Combinatorics
    Hugo Herbelin
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  9. coq-intuitionistic-nuprl

    No documentation

    An Impredicative Model of Nuprl's Constructive Type Theory
    keyword: Nuprl keyword: computational type theory keyword: extensional type theory keyword: intuitionistic type theory keyword: Howe's computational equivalence relation keyword: Partial Equivalence Relation (PER) semantics keyword: consistency keyword: continuity keyword: bar induction category: Mathematics/Logic/Type theory
    Vincent Rahli <vincent.rahli@gmail.com> [http://www.cs.cornell.edu/~rahli/] Abhishek Anand <abhishek.anand.iitg@gmail.com> [http://www.cs.cornell.edu/~aa755/] Mark Bickford <mark.concertina@gmail.com> [http://nuprl.org/]
    8.6.0
    GPL
    Used by 0 other packages
    20 Nov 2018
  10. 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
  11. coq-izf

    No documentation

    Intuitionistic Zermelo-Fraenkel Set Theory in Coq
    keyword: Intuitionistic set theory keyword: pointed graphs keyword: type theory keyword: intuitionistic choice operator keyword: set theory keyword: Zermelo-Fraenkel category: Mathematics/Logic/Set theory date: 2003-02
    Alexandre Miquel <Alexandre.Miquel@pps.jussieu.fr> [http://www.pps.jussieu.fr/~miquel]
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  12. 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
  13. coq-ltl

    No documentation

    Linear Temporal Logic
    keyword: temporal logic keyword: infinite transition systems keyword: co-induction category: Mathematics/Logic/Modal logic date: 2002-07
    Solange Coupet-Grimal
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  14. 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
  15. 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
  16. 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
  17. 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
  18. coq-ptsatr

    No documentation

    PTSATR
    keyword: pure type systems keyword: judgmental equality keyword: Church-Rosser keyword: confluence keyword: subject reduction keyword: pi injectivity category: Mathematics/Logic/Type theory
    Vincent Siles <vincent.siles@ens-lyon.org> [http://www.lix.polytechnique.fr/~vsiles] Hugo Herbelin <hugo.herbelin@inria.fr> [http://pauillac.inria.fr/~herbelin/]
    8.10.0
    LGPL
    Used by 1 other packages
    07 Dec 2019
  19. coq-ptsf

    No documentation

    Explicit Convertibility Proofs in Pure Type Systems
    keyword: pure type systems keyword: judgmental equality keyword: explicit equality proofs keyword: proof relevance category: Mathematics/Logic/Type theory
    Floris van Doorn <fpv@andrew.cmu.edu> [http://www.andrew.cmu.edu/user/fpv/] Herman Geuvers <herman@cs.ru.nl> [http://www.cs.ru.nl/~herman/] Freek Wiedijk <freek@cs.ru.nl> [http://www.cs.ru.nl/~freek/]
    8.10.0
    BSD
    Used by 0 other packages
    07 Dec 2019
  20. coq-ramsey

    No documentation

    Ramsey Theory
    keyword: dimension one Ramsey theorem keyword: constructive mathematics keyword: almost full sets category: Mathematics/Logic category: Mathematics/Combinatorics and Graph Theory category: Miscellaneous/Extracted Programs/Combinatorics
    Marc Bezem
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  21. coq-schroeder

    No documentation

    The Theorem of Schroeder-Bernstein
    keyword: Schroeder-Bernstein keyword: set theory category: Mathematics/Logic/Set theory
    Hugo herbelin
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  22. coq-tait

    No documentation

    A normalization proof a la Tait for simply-typed lambda-calculus
    keyword: normalization keyword: lambda calculus keyword: extraction keyword: Tait proof keyword: normalization by evalution keyword: type theory category: Mathematics/Logic/Type theory category: Computer Science/Lambda Calculi category: Miscellaneous/Extracted Programs/Type checking unification and normalization date: 2004
    Pierre Letouzey Helmut Schwichtenberg
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  23. coq-zf

    No documentation

    An axiomatisation of intuitionistic Zermelo-Fraenkel set theory
    keyword: set theory keyword: Zermelo-Fraenkel category: Mathematics/Logic/Set theory
    Guillaume Alexandre
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  24. coq-zfc

    No documentation

    An encoding of Zermelo-Fraenkel Set Theory in Coq
    keyword: set theory keyword: Zermelo-Fraenkel keyword: Calculus of Inductive Constructions category: Mathematics/Logic/Set theory
    Benjamin Werner
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019