11 search results for "tag:"keyword:automation""

Showing 1 - 11
  1. coq-formalv-check_range

    No documentation

    Tactics to automatically prove Boolean goals involving Uint63/Sint63 variables
    keyword:automation keyword:primitive integers logpath:formalv
    Ana de Almeida Borges Quim Casals Buñuel Juan Conejero Rodriguez Mireia González Bedmar Eduardo Hermo Reyes
    1.2.0
    PolyForm Noncommercial License 1.0.0
    Used by 1 other packages
    24 Jul 2023
  2. coq-geocoq

    No documentation

    A formalization of foundations of geometry in Coq
    category:Mathematics/Geometry/General keyword:geometry keyword:neutral geometry keyword:Euclidean geometry keyword:hyperbolic geometry keyword:foundations keyword:Tarski keyword:Hilbert keyword:Euclid keyword:Elements keyword:Pappus keyword:Desargues keyword:arithmetization keyword:Pythagoras keyword:Thales' intercept theorem keyword:continuity keyword:ruler and compass keyword:parallel postulates keyword:model keyword:counter-model keyword:Cartesian space keyword:automation date:2024-03-24
    Michael Beeson <profbeeson@gmail.com> Gabriel Braun <gabriel.braun@unistra.fr> Pierre Boutry <contact@pierre.boutry.fr> Cyril Cohen <cyril.cohen@inria.fr> Charly Gries <charly.gries@etu.unistra.fr> et al.
    2.5.0
    LGPL-3.0-only
    Used by 0 other packages
    25 Mar 2024
  3. coq-geocoq-coinc

    No documentation

    A formalization of foundations of geometry in Coq
    category:Mathematics/Geometry/General keyword:geometry keyword:automation date:2024-03-24
    Pierre Boutry <contact@pierre.boutry.fr> Julien Narboux <narboux@unistra.fr> Pascal Schreck <schreck@unistra.fr>
    2.5.0
    LGPL-3.0-only
    Used by 1 other packages
    25 Mar 2024
  4. coq-hammer

    No documentation

    General-purpose automated reasoning hammer tool for Coq
    category:Miscellaneous/Coq Extensions keyword:automation keyword:hammer logpath:Hammer.Plugin date:2024-11-15
    Lukasz Czajka <lukaszcz@mimuw.edu.pl> Cezary Kaliszyk <cezary.kaliszyk@uibk.ac.at>
    1.3.2+8.20
    LGPL-2.1-only
    Used by 1 other packages
    15 Nov 2024
  5. coq-hammer-tactics

    No documentation

    Reconstruction tactics for the hammer for Coq
    keyword:automation keyword:hammer keyword:tactics logpath:Hammer.Tactics date:2024-11-15
    Lukasz Czajka <lukaszcz@mimuw.edu.pl>
    1.3.2+8.20
    LGPL-2.1-only
    Used by 1 other packages
    15 Nov 2024
  6. 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
  7. coq-ppsimpl

    No documentation

    Ppsimpl is a reflexive tactic for canonising (arithmetic) goals
    keyword:integers keyword:arithmetic keyword:automation category:Miscellaneous/Coq Extensions logpath:PP
    Frédéric Besson
    8.10.0
    LGPL 3
    Used by 0 other packages
    18 Oct 2019
  8. coq-tactician

    No documentation

    Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq
    keyword:tactic-learning keyword:machine-learning keyword:automation keyword:proof-synthesis category:Miscellaneous/Coq Extensions logpath:Tactician
    Lasse Blaauwbroek <lasse@blaauwbroek.eu>
    1.0~beta2.1+8.19
    MIT
    Used by 1 other packages
    18 Jul 2024
  9. coq-tactician-dummy

    No documentation

    A dummy implementation of Tactician
    keyword:tactic-learning keyword:machine-learning keyword:automation keyword:proof-synthesis category:Miscellaneous/Coq Extensions logpath:Tactician
    Lasse Blaauwbroek <lasse@blaauwbroek.eu>
    1.0~beta2+8.17
    MIT
    Used by 1 other packages
    19 Oct 2023
  10. coq-tactician-stdlib

    No documentation

    Recompiles Coq's standard libary with Tactician's instrumentation loaded
    keyword:tactic-learning keyword:machine-learning keyword:automation keyword:proof-synthesis category:Miscellaneous/Coq Extensions logpath:Tactician
    Lasse Blaauwbroek <lasse@blaauwbroek.eu
    1.0~beta2+8.16
    MIT
    Used by 0 other packages
    19 Oct 2023
  11. 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