16 search results for "tag:"category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures""

Showing 1 - 16
  1. coq-aac-tactics

    No documentation

    Coq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators
    category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:reflexive tactic keyword:rewriting keyword:rewriting modulo associativity and commutativity keyword:rewriting modulo ac keyword:decision procedure logpath:AAC_tactics date:2024-06-27
    Thomas Braibant Damien Pous Fabian Kunze
    8.20.0
    LGPL-3.0-or-later
    Used by 2 other packages
    06 Sep 2024
  2. coq-atbr

    No documentation

    Coq library and tactic for deciding Kleene algebras
    category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:Kleene algebra keyword:finite automata keyword:semiring keyword:matrices keyword:decision procedure keyword:reflexive tactic logpath:ATBR date:2024-06-30
    Thomas Braibant Damien Pous
    8.20.0
    LGPL-3.0-or-later
    Used by 0 other packages
    06 Sep 2024
  3. coq-gappa

    No documentation

    A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover
    keyword:floating-point arithmetic keyword:interval arithmetic keyword:decision procedure category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:Gappa date:2025-06-11
    Guillaume Melquiond <guillaume.melquiond@inria.fr>
    1.7.1
    LGPL-3.0-or-later
    Used by 0 other packages
    12 Jun 2025
  4. coq-interval

    No documentation

    A Coq tactic for proving bounds on real-valued expressions automatically
    keyword:interval arithmetic keyword:decision procedure keyword:floating-point arithmetic keyword:reflexive tactic keyword:Taylor models category:Mathematics/Real Calculus and Topology category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:Interval date:2025-06-12
    Guillaume Melquiond <guillaume.melquiond@inria.fr> Érik Martin-Dorel <erik.martin-dorel@irit.fr> Pierre Roux <pierre.roux@onera.fr> Thomas Sibut-Pinote <thomas.sibut-pinote@inria.fr>
    4.11.2
    CeCILL-C
    Used by 7 other packages
    13 Jun 2025
  5. coq-itauto

    No documentation

    Reflexive SAT solver with Nelson-Oppen support, parameterised by a leaf tactic inside Coq
    category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:integers keyword:SAT keyword:SMT keyword:Nelson-Oppen keyword:automation logpath:Cdcl date:2024-06-17
    Frédéric Besson
    8.20.0
    MIT
    Used by 1 other packages
    06 Sep 2024
  6. coq-pil

    No documentation

    Coq library for Propositional Intuitionistic Logic & Pitts Interpolation Library
    date:2025-02-14 keyword:intuitionistic logic keyword:proof theory keyword:propositional quantifiers category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Mathematics/Logic/Foundations category:Mathematics/Logic/Modal logic logpath:ISL
    Hugo Férée Sam van Gool Yago Iglesias Vasquez
    1.0.1
    CECILL-2.1
    Used by 0 other packages
    26 Feb 2025
  7. coq-smtcoq

    No documentation

    A Coq plugin that checks proof witnesses coming from external SAT and SMT solvers
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword: SMT keyword: SAT keyword: automation logpath:SMTCoq
    Michaël Armand Valentin Blot Amina Bousalem Boris Djalal Louise Dubois de Prisque et al.
    2.3+8.20
    CECILL-C
    Used by 1 other packages
    19 Sep 2024
  8. coq-sniper

    No documentation

    A Coq plugin for general proof automation
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword: SMT keyword: automation logpath:Sniper
    Valentin Blot <Valentin.Blot@inria.fr> Louise Dubois de Prisque <Louise.Dubois-de-Prisque@inria.fr> Chantal Keller <ckeller@lmf.cnrs.fr Pierre Vial <Pierre.Vial@inria.fr>
    1.1+8.16
    CECILL-C
    Used by 0 other packages
    16 Jun 2023
  9. coq-stalmarck

    No documentation

    Verified implementation of Stålmarck's algorithm for proving tautologies in Coq
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:boolean formula keyword:tautology checker logpath:Stalmarck.Algorithm date:2024-06-30
    Pierre Letouzey Laurent Théry
    8.20.0
    LGPL-2.1-or-later
    Used by 1 other packages
    06 Sep 2024
  10. coq-trakt

    No documentation

    A generic goal preprocessing tool for proof automation tactics in Coq
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword:automation keyword:elpi date:2022-05-16 logpath:Trakt
    Enzo Crance
    1.2c
    LGPL-3.0-or-later
    Used by 0 other packages
    19 Jun 2024
  11. coq-trocq-hott

    No documentation

    A modular parametricity plugin for proof transfer in Coq
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword:automation keyword:elpi keyword:proof transfer keyword:isomorphism keyword:univalence keyword:parametricity logpath:Trocq
    Cyril Cohen Enzo Crance Lucie Lahaye Assia Mahboubi
    0.2.0
    LGPL-3.0-or-later
    Used by 1 other packages
    01 Jul 2025
  12. coq-trocq-hott-examples

    No documentation

    A modular parametricity plugin for proof transfer in Coq: examples
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword:automation keyword:elpi keyword:proof transfer keyword:isomorphism keyword:univalence keyword:parametricity logpath:Trocq
    Cyril Cohen Enzo Crance Lucie Lahaye Assia Mahboubi
    0.2.0
    LGPL-3.0-or-later
    Used by 0 other packages
    01 Jul 2025
  13. coq-trocq-std

    No documentation

    A modular parametricity plugin for proof transfer in Coq
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword:automation keyword:elpi keyword:proof transfer keyword:isomorphism keyword:univalence keyword:parametricity logpath:Trocq
    Cyril Cohen Enzo Crance Lucie Lahaye Assia Mahboubi
    0.2.0
    LGPL-3.0-or-later
    Used by 1 other packages
    01 Jul 2025
  14. coq-trocq-std-examples

    No documentation

    A modular parametricity plugin for proof transfer in Coq: examples
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword:automation keyword:elpi keyword:proof transfer keyword:isomorphism keyword:univalence keyword:parametricity logpath:Trocq
    Cyril Cohen Enzo Crance Lucie Lahaye Assia Mahboubi
    0.2.0
    LGPL-3.0-or-later
    Used by 0 other packages
    01 Jul 2025
  15. coq-vcfloat

    No documentation

    VCFloat: Floating Point Round-off Error Analysis
    date:2025-02-10 keyword:decision procedure keyword:floating-point arithmetic category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VCFloat
    Andrew W. Appel Ariel E. Kellison Tahina Ramananandro Paul Mountcastle Benoit Meister et al.
    2.3
    LGPL-3.0-or-later
    Used by 2 other packages
    10 Feb 2025
  16. coq-vst-lib

    No documentation

    VSTlib: VST-verified C library for VST-verified clients
    date:2025-02-10 keyword:VST keyword:library keyword:malloc keyword:threads keyword:floating-point arithmetic category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VSTlib
    Andrew W. Appel William Mansky
    2.15.1
    BSD-2-Clause
    Used by 0 other packages
    10 Feb 2025